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

def «term_ᶜ» : Lean.TrailingParserDescr

Set / lattice complement

Equations

• «term_ᶜ» = Lean.ParserDescr.trailingNode `term_ᶜ 1024 1024 (Lean.ParserDescr.symbol "ᶜ")

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

• BoxIntegral.Box.instSup
• FractionalIdeal.instSup
• OpenAddSubgroup.instSup
• OpenNormalAddSubgroup.instSupOfContinuousAdd
• OpenNormalSubgroup.instSupOfContinuousMul
• OpenSubgroup.instSup
• TwoSidedIdeal.instSup

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

• BoxIntegral.Box.WithBot.inf
• BoxIntegral.Prepartition.inf
• FractionalIdeal.instInf
• OpenAddSubgroup.instInfOpenAddSubgroup
• OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup
• OpenNormalSubgroup.instInfOpenNormalSubgroup
• OpenSubgroup.instInfOpenSubgroup
• TwoSidedIdeal.instInf

def «term_⊔_» : Lean.TrailingParserDescr

Least upper bound (\lub notation)

Equations

• «term_⊔_» = Lean.ParserDescr.trailingNode `term_⊔_ 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))

def «term_⊓_» : Lean.TrailingParserDescr

Greatest lower bound (\glb notation)

Equations

• «term_⊓_» = Lean.ParserDescr.trailingNode `term_⊓_ 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))

class HImp (α : Type u_1) : Type u_1

Syntax typeclass for Heyting implication ⇨.

• himp : α → α → α

  Heyting implication ⇨

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 ￢

def «term_⇨_» : Lean.TrailingParserDescr

Heyting implication

Equations

• «term_⇨_» = Lean.ParserDescr.trailingNode `term_⇨_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))

def «term￢_» : Lean.ParserDescr

Heyting negation

Equations

• «term￢_» = Lean.ParserDescr.node `term￢_ 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "￢") (Lean.ParserDescr.cat `term 72))

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

• OpenAddSubgroup.instTop
• OpenSubgroup.instTop
• TwoSidedIdeal.instTop
• ValuationSubring.instTop
• instTop𝓓

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

• TwoSidedIdeal.instBot
• instBotLevenshteinEstimator
• instBotTrivial
• instBot𝓓

def «term⊤» : Lean.ParserDescr

The top (⊤, \top) element

Equations

• «term⊤» = Lean.ParserDescr.node `term⊤ 1024 (Lean.ParserDescr.symbol "⊤")

def «term⊥» : Lean.ParserDescr

The bot (⊥, \bot) element

Equations

• «term⊥» = Lean.ParserDescr.node `term⊥ 1024 (Lean.ParserDescr.symbol "⊥")

@[instance 100]

instance top_nonempty (α : Type u_1) [Top α] : Nonempty α

Equations

• ⋯ = ⋯

@[instance 100]

instance bot_nonempty (α : Type u_1) [Bot α] : Nonempty α

Equations

• ⋯ = ⋯