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
    Instances For

      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
          Instances For

            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
            Instances For

              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.
              Instances For

                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.
                Instances For
                  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

                      Heyting implication

                      Equations
                      Instances For

                        Heyting negation

                        Equations
                        Instances For
                          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
                              Instances For

                                The bot (, \bot) element

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