Notation classes for lattice operations #
In this file we introduce typeclasses and definitions for lattice operations.
Main definitions #
HasCompl
: type class for theᶜ
notationTop
: type class for the⊤
notationBot
: type class for the⊥
notation
Notations #
xᶜ
: complement in a lattice;x ⊔ y
: supremum/join, which is notation formax x y
;x ⊓ y
: infimum/meet, which is notation formin 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.
Set / lattice complement
Equations
- «term_ᶜ» = Lean.ParserDescr.trailingNode `«term_ᶜ» 1024 1024 (Lean.ParserDescr.symbol "ᶜ")
Instances For
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
- «term_⊔_» = Lean.ParserDescr.trailingNode `«term_⊔_» 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))
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
- «term_⊓_» = Lean.ParserDescr.trailingNode `«term_⊓_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))
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
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
- «term_⇨_» = Lean.ParserDescr.trailingNode `«term_⇨_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))
Instances For
Heyting negation
Equations
- «term¬_» = Lean.ParserDescr.node `«term¬_» 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 72))
Instances For
The top (⊤
, \top
) element
Equations
- «term⊤» = Lean.ParserDescr.node `«term⊤» 1024 (Lean.ParserDescr.symbol "⊤")
Instances For
The bot (⊥
, \bot
) element
Equations
- «term⊥» = Lean.ParserDescr.node `«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")