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

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

                        Equations
                          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 α] :