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 #

      theorem Min.ext {α : Type u} {x y : Min α} (min : min = min) :
      x = y
      theorem Max.ext_iff {α : Type u} {x y : Max α} :
      x = y max = max
      theorem Min.ext_iff {α : Type u} {x y : Min α} :
      x = y min = min
      theorem Max.ext {α : Type u} {x y : Max α} (max : max = max) :
      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 α] :