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 ⊔.

theorem Lean.Order.le_himp_of_meet_le_left {α : 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.

Derived laws

Connectives

theorem Lean.Order.le_himp {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.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_left {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.join_meet_le {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 {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.CompleteLattice.ofProp_imp_le_himp {l : Type u} [CompleteLattice l] [Heyting l] {φ₁ φ₂ : Prop} : PartialOrder.rel (ofProp (φ₁ → φ₂)) (himp (ofProp φ₁) (ofProp φ₂))

@[simp]

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

@[deprecated Lean.Order.CompleteLattice.ofProp_imp_le_himp (since := "2026-09-24")]

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

@[deprecated Lean.Order.CompleteLattice.ofProp_himp_ofProp (since := "2026-09-24")]

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

@[deprecated Lean.Order.join_meet_le (since := "2026-09-24")]

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

@[deprecated Lean.Order.meet_join_le (since := "2026-09-24")]

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

@[deprecated Lean.Order.le_himp (since := "2026-09-24")]

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)

@[deprecated Lean.Order.le_himp_of_meet_le_left (since := "2026-09-24")]

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)

@[deprecated Lean.Order.meet_le_of_le_himp_left (since := "2026-09-24")]

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

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