Heyting implication

a ⇨ b is the upper adjoint of the lattice meet a ⊓ ·. A complete lattice whose meet preserves suprema is a frame, and ⇨ then satisfies the laws of an implication: modus ponens, currying and distribution of ⊓ over ⊔.

@[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.

Equations

• Lean.Order.Heyting α = ∀ (a : α), Lean.Order.PreservesSup (Lean.Order.meet a)

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

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

Equations

• Lean.Order.himp a b = Lean.Order.PreservesSup.upperAdjoint (Lean.Order.meet a) b

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

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

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.le_himp {α : Type u} [CompleteLattice α] {a b x : α} (h : PartialOrder.rel (meet a x) b) : PartialOrder.rel x (himp a b)

Unit for ⇨, the meet specialization of PreservesSup.le_upperAdjoint: a ⊓ x ⊑ b → x ⊑ a ⇨ b.

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

Counit for ⇨, the meet specialization of PreservesSup.upperAdjoint_le: a ⊓ (a ⇨ b) ⊑ b.

@[simp]

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

@[simp]

theorem Lean.Order.himp_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.

Derived laws

Connectives

theorem Lean.Order.le_himp_comm {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] (h : PartialOrder.rel (meet P Q) R) : PartialOrder.rel P (himp Q R)

theorem Lean.Order.le_himp_of_meet_le_comm {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] (h : PartialOrder.rel (meet Q P) R) : PartialOrder.rel P (himp Q R)

theorem Lean.Order.meet_le_of_le_himp {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] (h : PartialOrder.rel P (himp Q R)) : PartialOrder.rel (meet P Q) R

theorem Lean.Order.meet_le_of_le_himp_comm {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] (h : PartialOrder.rel Q (himp P R)) : PartialOrder.rel (meet P Q) R

theorem Lean.Order.himp_meet_le {l : Type u} [CompleteLattice l] {P Q : l} [Heyting l] : PartialOrder.rel (meet (himp P Q) P) Q

theorem Lean.Order.le_himp_mp {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] (h₁ : PartialOrder.rel P (himp Q R)) (h₂ : PartialOrder.rel P Q) : PartialOrder.rel P R

theorem Lean.Order.meet_join_le_left {l : Type u} [CompleteLattice l] {P Q R T : l} [Heyting l] (hleft : PartialOrder.rel (meet P R) T) (hright : PartialOrder.rel (meet Q R) T) : PartialOrder.rel (meet (join P Q) R) T

theorem Lean.Order.meet_join_le_right {l : Type u} [CompleteLattice l] {P Q R T : l} [Heyting l] (hleft : PartialOrder.rel (meet P Q) T) (hright : PartialOrder.rel (meet P R) T) : PartialOrder.rel (meet P (join Q R)) T

Monotonicity

theorem Lean.Order.himp_mono {l : Type u} [CompleteLattice l] {P P' Q Q' : l} [Heyting l] (h1 : PartialOrder.rel Q P) (h2 : PartialOrder.rel P' Q') : PartialOrder.rel (himp P P') (himp Q Q')

theorem Lean.Order.himp_mono_left {l : Type u} [CompleteLattice l] {P P' Q : l} [Heyting l] (h : PartialOrder.rel P' P) : PartialOrder.rel (himp P Q) (himp P' Q)

theorem Lean.Order.himp_mono_right {l : Type u} [CompleteLattice l] {P Q Q' : l} [Heyting l] (h : PartialOrder.rel Q Q') : PartialOrder.rel (himp P Q) (himp P Q')

Distributivity

theorem Lean.Order.meet_join_left {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] : meet P (join Q R) = join (meet P Q) (meet P R)

theorem Lean.Order.join_meet_left {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] : join P (meet Q R) = meet (join P Q) (join P R)

theorem Lean.Order.meet_join_right {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] : meet (join P Q) R = join (meet P R) (meet Q R)

theorem Lean.Order.join_meet_right {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] : join (meet P Q) R = meet (join P R) (join Q R)

Units and composition

theorem Lean.Order.top_himp {l : Type u} [CompleteLattice l] {P : l} [Heyting l] : himp top P = P

theorem Lean.Order.le_himp_self {l : Type u} [CompleteLattice l] {P Q : l} [Heyting l] : PartialOrder.rel Q (himp P P)

theorem Lean.Order.le_himp_self_iff {l : Type u} [CompleteLattice l] {P Q : l} [Heyting l] : PartialOrder.rel Q (himp P P) ↔ True

theorem Lean.Order.himp_meet_himp_le {l : Type u} [CompleteLattice l] {P Q R : l} [Heyting l] : PartialOrder.rel (meet (himp P Q) (himp Q R)) (himp P R)

theorem Lean.Order.bot_himp {l : Type u} [CompleteLattice l] {P : l} [Heyting l] : himp bot P = top

theorem Lean.Order.meet_himp_le_meet {l : Type u} [CompleteLattice l] {P' Q' : l} [Heyting l] : PartialOrder.rel (meet P' (himp P' Q')) (meet P' Q')

theorem Lean.Order.meet_le_meet_of_le_himp {l : Type u} [CompleteLattice l] {P P' Q Q' : l} [Heyting l] (hp : PartialOrder.rel P P') (hq : PartialOrder.rel Q (himp P' Q')) : PartialOrder.rel (meet P Q) (meet P' Q')

Interaction with the propositional embedding

theorem Lean.Order.himp_ofProp_le {l : Type u} [CompleteLattice l] [Heyting l] {φ₁ φ₂ : Prop} : PartialOrder.rel (CompleteLattice.ofProp (φ₁ → φ₂)) (himp (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂))

theorem Lean.Order.himp_ofProp {l : Type u} [CompleteLattice l] [Heyting l] {φ₁ φ₂ : Prop} : himp (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂) = CompleteLattice.ofProp (φ₁ → φ₂)

@[simp]

theorem Lean.Order.top_le_himp_iff {l : Type u} [CompleteLattice l] [Heyting l] (P Q : l) : PartialOrder.rel top (himp P Q) ↔ PartialOrder.rel P Q

⊤ ⊑ (P ⇨ Q) iff P ⊑ Q.