Additional operations of a complete lattice

The top element ⊤, the binary meet ⊓ and join ⊔, and the indexed infimum ⨅ and supremum ⨆. The bottom element ⊥ comes from CCPO, which every complete lattice is.

noncomputable def Lean.Order.top {α : Type u} [CompleteLattice α] : α

Top element of a complete lattice (supremum of all elements)

Equations

• Lean.Order.top = Lean.Order.CompleteLattice.sup fun (x : α) => True

def Lean.Order.«term⊤» : ParserDescr

Top element of a complete lattice (supremum of all elements)

Equations

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

@[instance_reducible]

noncomputable def Lean.Order.instCCPOOfCompleteLattice {α : Type u} [CompleteLattice α] : CCPO α

A complete lattice is a chain-complete partial order.

Equations

• Lean.Order.instCCPOOfCompleteLattice = { toPartialOrder := inst✝.toPartialOrder, has_csup := ⋯ }

noncomputable def Lean.Order.meet {α : Type u} [CompleteLattice α] (x y : α) : α

Binary meet (infimum)

Equations

• Lean.Order.meet x y = Lean.Order.inf fun (z : α) => z = x ∨ z = y

def Lean.Order.«term_⊓_» : TrailingParserDescr

Binary meet (infimum)

Equations

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

noncomputable def Lean.Order.join {α : Type u} [CompleteLattice α] (x y : α) : α

Binary join (supremum)

Equations

• Lean.Order.join x y = Lean.Order.CompleteLattice.sup fun (z : α) => z = x ∨ z = y

def Lean.Order.«term_⊔_» : TrailingParserDescr

Binary join (supremum)

Equations

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

noncomputable def Lean.Order.iInf {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) : α

Indexed infimum

Equations

• Lean.Order.iInf f = Lean.Order.inf fun (x : α) => ∃ (i : ι), f i = x

def Lean.Order.«term⨅_,_» : ParserDescr

Indexed infimum

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Lean.Order.iSup {α : Type u} [CompleteLattice α] {ι : Type v} (f : ι → α) : α

Indexed supremum

Equations

• Lean.Order.iSup f = Lean.Order.CompleteLattice.sup fun (x : α) => ∃ (i : ι), f i = x

def Lean.Order.«term⨆_,_» : ParserDescr

Indexed supremum

Equations

• One or more equations did not get rendered due to their size.