Documentation

Mathlib.Order.Notation

Notation classes for lattice operations #

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

Main definitions #

Notations #

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 Sup.ext {α : Type u_1} {x : Sup α} {y : Sup α} (sup : Sup.sup = Sup.sup) :
      x = y
      theorem Sup.ext_iff {α : Type u_1} {x : Sup α} {y : Sup α} :
      x = y Sup.sup = Sup.sup
      class Sup (α : Type u_1) :
      Type u_1

      Typeclass for the (\lub) notation

      • sup : ααα

        Least upper bound (\lub notation)

      Instances
        theorem Inf.ext {α : Type u_1} {x : Inf α} {y : Inf α} (inf : Inf.inf = Inf.inf) :
        x = y
        theorem Inf.ext_iff {α : Type u_1} {x : Inf α} {y : Inf α} :
        x = y Inf.inf = Inf.inf
        class Inf (α : Type u_1) :
        Type u_1

        Typeclass for the (\glb) notation

        • inf : ααα

          Greatest lower bound (\glb notation)

        Instances

          Least upper bound (\lub notation)

          Equations
          Instances For

            Greatest lower bound (\glb notation)

            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 negation

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

                    Typeclass for the (\top) notation

                    • top : α

                      The top (, \top) element

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

                      Typeclass for the (\bot) notation

                      • bot : α

                        The bot (, \bot) element

                      Instances

                        The top (, \top) element

                        Equations
                        Instances For

                          The bot (, \bot) element

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