Complete lattices

The definitions and instances of the lattice theory: the operations of a complete lattice, the complete lattice of propositions, the embedding ⌜·⌝ of propositions, supremum-preserving maps with their upper adjoints, and Heyting implication ⇨.

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)

def Lean.Order.«term⊤» : ParserDescr

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

@[instance_reducible]

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

A complete lattice is a chain-complete partial order.

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

Binary meet (infimum)

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

Binary meet (infimum)

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

Binary join (supremum)

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

Binary join (supremum)

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

Indexed infimum

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

Indexed infimum

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

Indexed supremum

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

Indexed supremum

The complete lattice of propositions

⊑ is implication and the supremum of a set of propositions is the existential quantifier over it.

The instances are scoped in Std.Internal.Order, outside of Lean.Order. partial_fixpoint and coinductive_fixpoint order Prop by ImplicationOrder and ReverseImplicationOrder, and their monotonicity lemmas live in Lean.Order itself. Open Std.Internal.Order to order Prop by implication.

@[instance_reducible]

def Std.Internal.Order.instPartialOrderProp : Lean.Order.PartialOrder Prop

def Std.Internal.Order.propSup (c : Prop → Prop) : Prop

Supremum for Prop: true iff some element of the set is true

theorem Std.Internal.Order.propSup_is_sup (c : Prop → Prop) : Lean.Order.is_sup c (propSup c)

@[instance_reducible]

def Std.Internal.Order.instCompleteLatticeProp : Lean.Order.CompleteLattice Prop

Embedding of propositions

⌜p⌝ embeds a proposition p into an assertion lattice as ⊤ if p holds and ⊥ otherwise.

noncomputable def Lean.Order.CompleteLattice.ofProp {l : Type u_1} [CompleteLattice l] (p : Prop) : l

Embedding of propositions into an CompleteLattice type. ⌜p⌝ embeds p : Prop as ⊤ if p holds and ⊥ otherwise.

def Lean.Order.«term⌜_⌝» : ParserDescr

Embedding of propositions into an CompleteLattice type. ⌜p⌝ embeds p : Prop as ⊤ if p holds and ⊥ otherwise.

Supremum-preserving maps and Heyting implication

A supremum-preserving map on a complete lattice is a lower adjoint. Its upper adjoint is the implication belonging to it: Heyting ⇨ for the lattice meet, a magic wand for a separating conjunction.

class Lean.Order.PreservesSup {α : Type u} [CompleteLattice α] (f : α → α) : Prop

f : α → α preserves suprema if it distributes over arbitrary suprema: f (sup s) = sup { f x | x ∈ s }. Equivalently f is a lower adjoint, so it has an upper adjoint PreservesSup.upperAdjoint f.

A frame operator acts by a supremum-preserving map for each resource r: the lattice meet (a ⊓ ·), or a cost combinator (costConj r) for a counter resource. The upper adjoint is the corresponding implication: Heyting ⇨ for the meet, a magic wand for separating conjunction.

• map_sup (s : α → Prop) : f (CompleteLattice.sup s) = CompleteLattice.sup fun (y : α) => ∃ (x : α), s x ∧ y = f x

  f preserves joins.

noncomputable def Lean.Order.PreservesSup.upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : α

The upper adjoint of f: the join of all x with f x ⊑ b. For f = (a ⊓ ·) this is Heyting implication a ⇨ ·.

theorem Lean.Order.PreservesSup.le_upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) {b x : α} (h : PartialOrder.rel (f x) b) : PartialOrder.rel x (upperAdjoint f b)

Unit, free from the definition of upperAdjoint: f x ⊑ b → x ⊑ upperAdjoint f b. Needs only CompleteLattice.

@[reducible, inline]

abbrev Lean.Order.Heyting (α : Type u) [CompleteLattice α] : Prop

A complete lattice whose meets preserve suprema. The Heyting implication ⇨ is then a right adjoint, and ⊓ distributes over suprema of arbitrary families. The literature also calls such a lattice a frame.

noncomputable def Lean.Order.himp {α : Type u} [CompleteLattice α] (a b : α) : α

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.

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

Heyting implication: the upper adjoint of the lattice meet. For Prop it is →.