# Notation classes for lattice operations #

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

## Main definitions #

• Sup: type class for the ⊔ notation
• Inf: type class for the ⊓ notation
• HasCompl: type class for the ᶜ notation
• Top: type class for the ⊤ notation
• Bot: type class for the ⊥ notation

## Notations #

• x ⊔ y: lattice join operation;
• x ⊓ y: lattice meet operation;
• xᶜ: complement in a lattice;
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_iff {α : Type u_1} (x : Inf α) (y : Inf α) :
x = y Inf.inf = Inf.inf
theorem Inf.ext {α : Type u_1} (x : Inf α) (y : Inf α) (inf : Inf.inf = Inf.inf) :
x = y
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 implication

Equations
Instances For

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_iff {α : Type u_1} (x : Bot α) (y : Bot α) :
x = y
theorem Bot.ext {α : Type u_1} (x : Bot α) (y : Bot α) (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
• =