class Lean.Order.Frame (α : Type u) [CompleteLattice α] : Prop

A complete lattice is a frame if binary meet distributes over arbitrary joins (the frame law). This matches the Mathlib definition Order.Frame.

We keep CompleteLattice as a parameter (instead of extending it), so the class only adds the frame law.

• meet_sup (a : α) (s : α → Prop) : meet a (CompleteLattice.sup s) = CompleteLattice.sup fun (y : α) => ∃ (x : α), s x ∧ y = meet a x

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

Heyting implication in a frame, defined as the join of all x such that a ⊓ x ⊑ b.

Equations

• Lean.Order.himp a b = Lean.Order.CompleteLattice.sup fun (x : α) => Lean.Order.PartialOrder.rel (Lean.Order.meet a x) b

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

Equations

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

theorem Lean.Order.himp_spec {α : Type u} [CompleteLattice α] (a b : α) : is_sup (fun (x : α) => PartialOrder.rel (meet a x) b) (himp a b)

a ⇨ b is the least upper bound of {x | a ⊓ x ⊑ b} by definition.

theorem Lean.Order.himp_complete {α : Type u} [CompleteLattice α] (x a b : α) : PartialOrder.rel (meet a x) b → PartialOrder.rel x (himp a b)

Completeness direction that only needs CompleteLattice: if a ⊓ x ⊑ b, then x ⊑ a ⇨ b.

theorem Lean.Order.himp_sound {α : Type u} [CompleteLattice α] [Frame α] (a b : α) : PartialOrder.rel (meet a (himp a b)) b

Soundness direction (a ⊓ (a ⇨ b) ⊑ b) from the frame distributivity law.

@[simp]

theorem Lean.Order.himp_prop_eq_imp (a b : Prop) : himp a b = (a → b)

@[simp]

theorem Lean.Order.himp_fun_apply {σ : Type v} {β : Type u} [CompleteLattice β] (a b : σ → β) (s : σ) : himp a b s = himp (a s) (b s)

Pointwise characterization of Heyting implication on function lattices.