Documentation

Mathlib.Order.Notation

Notation classes for lattice operations #

In this file we introduce typeclasses and definitions for lattice operations.

Main definitions #

Notations #

We implement a delaborator that pretty prints max x y/min x y as x ⊔ y/x ⊓ y if and only if the order on α does not have a LinearOrder α instance (where x y : α).

This is so that in a lattice we can use the same underlying constants max/min as in linear orders, while using the more idiomatic notation x ⊔ y/x ⊓ y. Lemmas about the operators and should use the names sup and inf respectively.

class HasCompl (α : Type u_1) :
Type u_1

Set / lattice complement

  • compl : αα

    Set / lattice complement

Instances

    Set / lattice complement

    Equations

    Sup and Inf #

    @[deprecated Max (since := "2024-11-06")]
    class Sup (α : Type u_1) :
    Type u_1

    Typeclass for the (\lub) notation

    • sup : ααα

      Least upper bound (\lub notation)

    Instances
      theorem Sup.ext_iff {α : Type u_1} {x y : Sup α} :
      x = y sup = sup
      theorem Sup.ext {α : Type u_1} {x y : Sup α} (sup : sup = sup) :
      x = y
      @[deprecated Min (since := "2024-11-06")]
      class Inf (α : Type u_1) :
      Type u_1

      Typeclass for the (\glb) notation

      • inf : ααα

        Greatest lower bound (\glb notation)

      Instances
        theorem Inf.ext {α : Type u_1} {x y : Inf α} (inf : inf = inf) :
        x = y
        theorem Inf.ext_iff {α : Type u_1} {x y : Inf α} :
        x = y inf = inf
        theorem Max.ext {α : Type u} {x y : Max α} (max : max = max) :
        x = y
        theorem Min.ext_iff {α : Type u} {x y : Min α} :
        x = y min = min
        theorem Max.ext_iff {α : Type u} {x y : Max α} :
        x = y max = max
        theorem Min.ext {α : Type u} {x y : Min α} (min : min = min) :
        x = y

        The supremum/join operation: x ⊔ y. It is notation for max x y and should be used when the type is not a linear order.

        Equations

        The infimum/meet operation: x ⊓ y. It is notation for min x y and should be used when the type is not a linear order.

        Equations

        Delaborate max x y into x ⊔ y if the type is not a linear order.

        Equations
        • One or more equations did not get rendered due to their size.

        Delaborate min x y into x ⊓ y if the type is not a linear order.

        Equations
        • One or more equations did not get rendered due to their size.
        class HImp (α : Type u_1) :
        Type u_1

        Syntax typeclass for Heyting implication .

        • himp : ααα

          Heyting implication

        Instances
          class HNot (α : Type u_1) :
          Type u_1

          Syntax typeclass for Heyting negation .

          The difference between HasCompl and HNot is that the former belongs to Heyting algebras, while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl underestimates while HNot overestimates. In boolean algebras, they are equal. See hnot_eq_compl.

          • hnot : αα

            Heyting negation

          Instances
            class Top (α : Type u_1) :
            Type u_1

            Typeclass for the (\top) notation

            • top : α

              The top (, \top) element

            Instances
              theorem Top.ext_iff {α : Type u_1} {x y : Top α} :
              x = y =
              theorem Top.ext {α : Type u_1} {x y : Top α} (top : = ) :
              x = y
              class Bot (α : Type u_1) :
              Type u_1

              Typeclass for the (\bot) notation

              • bot : α

                The bot (, \bot) element

              Instances
                theorem Bot.ext_iff {α : Type u_1} {x y : Bot α} :
                x = y =
                theorem Bot.ext {α : Type u_1} {x y : Bot α} (bot : = ) :
                x = y

                The top (, \top) element

                Equations

                The bot (, \bot) element

                Equations
                @[instance 100]
                instance top_nonempty (α : Type u_1) [Top α] :
                @[instance 100]
                instance bot_nonempty (α : Type u_1) [Bot α] :