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.

source
class HasCompl (α : Type u_1) :
Type u_1

Set / lattice complement

  • compl : α → α

    Set / lattice complement

Instances
source
def «term_ᶜ» :
Lean.TrailingParserDescr

Set / lattice complement

Equations

Sup and Inf #

source
@[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
    source
    theorem Sup.ext_iff {α : Type u_1} {x y : Sup α} :
    x = y ↔ sup = sup
    source
    theorem Sup.ext {α : Type u_1} {x y : Sup α} (sup : sup = sup) :
    x = y
    source
    @[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
      source
      theorem Inf.ext {α : Type u_1} {x y : Inf α} (inf : inf = inf) :
      x = y
      source
      theorem Inf.ext_iff {α : Type u_1} {x y : Inf α} :
      x = y ↔ inf = inf
      source
      theorem Max.ext {α : Type u} {x y : Max α} (max : max = max) :
      x = y
      source
      theorem Min.ext_iff {α : Type u} {x y : Min α} :
      x = y ↔ min = min
      source
      theorem Max.ext_iff {α : Type u} {x y : Max α} :
      x = y ↔ max = max
      source
      theorem Min.ext {α : Type u} {x y : Min α} (min : min = min) :
      x = y
      source
      def «term_⊔_» :
      Lean.TrailingParserDescr

      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
      source
      def «term_⊓_» :
      Lean.TrailingParserDescr

      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
      source
      def Mathlib.Meta.delabSup :
      Lean.PrettyPrinter.Delaborator.Delab

      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.
      source
      def Mathlib.Meta.delabInf :
      Lean.PrettyPrinter.Delaborator.Delab

      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.
      source
      class HImp (α : Type u_1) :
      Type u_1

      Syntax typeclass for Heyting implication ⇨.

      • himp : α → α → α

        Heyting implication ⇨

      Instances
      source
      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
      source
      def «term_⇨_» :
      Lean.TrailingParserDescr

      Heyting implication

      Equations
      source
      def «term￢_» :
      Lean.ParserDescr

      Heyting negation

      Equations
      source
      class Top (α : Type u_1) :
      Type u_1

      Typeclass for the ⊤ (\top) notation

      • top : α

        The top (⊤, \top) element

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

      Typeclass for the ⊥ (\bot) notation

      • bot : α

        The bot (⊥, \bot) element

      Instances
      source
      theorem Bot.ext_iff {α : Type u_1} {x y : Bot α} :
      x = y ↔ ⊥ = ⊥
      source
      theorem Bot.ext {α : Type u_1} {x y : Bot α} (bot : ⊥ = ⊥) :
      x = y
      source
      def «term⊤» :
      Lean.ParserDescr

      The top (⊤, \top) element

      Equations
      source
      def «term⊥» :
      Lean.ParserDescr

      The bot (⊥, \bot) element

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