doc-next-gen

Mathlib.Order.Notation

Module docstring

{"# Notation classes for lattice operations

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

Main definitions

  • HasCompl: type class for the ᶜ notation
  • Top: type class for the ⊤ notation
  • Bot: type class for the ⊥ notation

Notations

  • xᶜ: complement in a lattice;
  • x ⊔ y: supremum/join, which is notation for max x y;
  • x ⊓ y: infimum/meet, which is notation for min x y;

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.

","### Sup and Inf "}

HasCompl structure
(α : Type*)
Full source 
/-- Set / lattice complement -/
@[notation_class]
class HasCompl (α : Type*) where
  /-- Set / lattice complement -/
  compl : α → α
Complement notation in lattices and sets
Informal description
The structure `HasCompl` is a typeclass that provides the notation `ᶜ` for the complement operation in a lattice or set. It is used to denote the complement of an element in a lattice or a set.
term_ᶜ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc]
postfix:1024 "ᶜ" => compl
Complement notation in a lattice
Informal description
The postfix notation `ᶜ` is defined to represent the complement operation in a lattice, where for an element `x` in the lattice, `xᶜ` denotes its complement.
Sup structure
(α : Type*)
Full source 
/-- Typeclass for the `⊔` (`\lub`) notation -/
@[deprecated Max (since := "2024-11-06"), notation_class, ext]
class Sup (α : Type*) where
  /-- Least upper bound (`\lub` notation) -/
  sup : α → α → α
Supremum operation
Informal description
The structure representing the typeclass for the supremum operation `⊔` (join) on a type `α`.
Inf structure
(α : Type*)
Full source 
/-- Typeclass for the `⊓` (`\glb`) notation -/
@[deprecated Min (since := "2024-11-06"), notation_class, ext]
class Inf (α : Type*) where
  /-- Greatest lower bound (`\glb` notation) -/
  inf : α → α → α
Infimum operation in a lattice
Informal description
The structure representing the infimum operation in a lattice, denoted by the symbol `⊓` (read as "meet"). For any type `α`, this operation takes two elements of `α` and returns their greatest lower bound.
term_⊓_ definition
: Lean.TrailingParserDescr✝
Full source 
/--
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.
-/
syntax:69 term:69 " ⊓ " term:70 : term
Infimum/meet operation in a lattice
Informal description
The infimum/meet operation between two elements $x$ and $y$ in a lattice, denoted by $x ⊓ y$. This notation is equivalent to the minimum operation $\min(x, y)$ and is used when the type does not have a linear order structure.
Mathlib.Meta.delabSup definition
: Delab
Full source 
/-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order. -/
@[delab app.Max.max]
def delabSup : Delab := do
  let_expr [email protected] α inst _ _ := ← getExpr | failure
  have u := f.constLevels![0]!
  if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
    failure -- use the default delaborator
  let x ← withNaryArg 2 delab
  let y ← withNaryArg 3 delab
  let stx ← `($x ⊔ $y)
  annotateGoToSyntaxDef stx
Supremum notation delaborator
Informal description
The delaborator converts the expression `max x y` into the notation `x ⊔ y` (representing the supremum/join operation) when the type `α` does not have a linear order instance. If `α` has a linear order, the delaborator fails and falls back to the default delaborator for `max`.
Mathlib.Meta.delabInf definition
: Delab
Full source 
/-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order. -/
@[delab app.Min.min]
def delabInf : Delab := do
  let_expr [email protected] α inst _ _ := ← getExpr | failure
  have u := f.constLevels![0]!
  if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
    failure -- use the default delaborator
  let x ← withNaryArg 2 delab
  let y ← withNaryArg 3 delab
  let stx ← `($x ⊓ $y)
  annotateGoToSyntaxDef stx
Infimum notation delaborator
Informal description
The delaborator converts the expression `min x y` into the notation `x ⊓ y` (representing the infimum/meet operation) when the type `α` does not have a linear order instance. If `α` has a linear order, the delaborator fails and falls back to the default delaborator for `min`.
HImp structure
(α : Type*)
Full source 
/-- Syntax typeclass for Heyting implication `⇨`. -/
@[notation_class]
class HImp (α : Type*) where
  /-- Heyting implication `⇨` -/
  himp : α → α → α
Heyting implication syntax
Informal description
The structure representing the syntax typeclass for Heyting implication `⇨` in a type `α`.
HNot structure
(α : Type*)
Full source 
/-- 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`.
-/
@[notation_class]
class HNot (α : Type*) where
  /-- Heyting negation `￢` -/
  hnot : α → α
Heyting Negation Syntax Typeclass
Informal description
The structure representing the syntax typeclass for Heyting negation `¬` in co-Heyting algebras. Unlike the `HasCompl` notation which belongs to Heyting algebras and provides a pseudo-complement that underestimates, `HNot` provides a pseudo-complement that overestimates. In boolean algebras, these two notions coincide.
term_⇨_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Heyting implication -/
infixr:60 " ⇨ " => himp
Heyting implication
Informal description
The notation `⇨` represents Heyting implication, a binary operation on a type `α` that generalizes classical implication to intuitionistic logic. For elements `a` and `b` of `α`, the expression `a ⇨ b` denotes the Heyting implication of `a` and `b`.
term￢_ definition
: Lean.ParserDescr✝
Full source 
/-- Heyting negation -/
prefix:72 "￢" => hnot
Heyting negation
Informal description
The notation `￢` represents Heyting negation, a logical operation in intuitionistic logic. For a proposition `p`, `￢p` denotes the negation of `p` in the Heyting algebra sense, which is defined as `p → ⊥` (where `⊥` is the false proposition).
Top structure
(α : Type*)
Full source 
/-- Typeclass for the `⊤` (`\top`) notation -/
@[notation_class, ext]
class Top (α : Type*) where
  /-- The top (`⊤`, `\top`) element -/
  top : α
Top element in a lattice
Informal description
The structure `Top` represents a typeclass for the notation `⊤` (top element) in a lattice or ordered structure. It provides a distinguished element that is greater than or equal to all other elements in the type `α`.
Bot structure
(α : Type*)
Full source 
/-- Typeclass for the `⊥` (`\bot`) notation -/
@[notation_class, ext]
class Bot (α : Type*) where
  /-- The bot (`⊥`, `\bot`) element -/
  bot : α
Bottom element typeclass
Informal description
The structure representing the typeclass for the bottom element notation `⊥` in a lattice or ordered set.
term⊤ definition
: Lean.ParserDescr✝
Full source 
/-- The top (`⊤`, `\top`) element -/
notation "⊤" => Top.top
Top element notation (`⊤`)
Informal description
The notation `⊤` represents the top element in a lattice or ordered structure, which is the greatest element in the type with respect to the order relation.
top_nonempty instance
(α : Type*) [Top α] : Nonempty α
Full source 
instance (priority := 100) top_nonempty (α : Type*) [Top α] : Nonempty α :=
  ⟨⊤⟩
Nonemptiness from Top Element
Informal description
For any type $\alpha$ equipped with a top element $\top$, the type $\alpha$ is nonempty.
bot_nonempty instance
(α : Type*) [Bot α] : Nonempty α
Full source 
instance (priority := 100) bot_nonempty (α : Type*) [Bot α] : Nonempty α :=
  ⟨⊥⟩
Nonemptiness from Bottom Element
Informal description
For any type $\alpha$ equipped with a bottom element $\bot$, the type $\alpha$ is nonempty.