Laws of the embedding of propositions

⌜p⌝ embeds a proposition p into an assertion lattice as ⊤ if p holds and ⊥ otherwise. It is a homomorphism from the connectives of Prop to the lattice operations, and it is monotone.

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_true (l : Type v) [CompleteLattice l] : ofProp True = top

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_false (l : Type v) [CompleteLattice l] : ofProp False = bot

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_le_eq_imp {l : Type u_1} [CompleteLattice l] (p : Prop) (h : l) : PartialOrder.rel (ofProp p) h = (p → PartialOrder.rel top h)

@[simp]

theorem Lean.Order.CompleteLattice.meet_ofProp_le_eq_imp {l : Type u_1} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet x (ofProp p)) y = (p → PartialOrder.rel x y)

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_meet_le_eq_imp {l : Type u_1} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet (ofProp p) x) y = (p → PartialOrder.rel x y)

theorem Lean.Order.CompleteLattice.top_le_ofProp {l : Type u_1} [CompleteLattice l] (p : Prop) : p → PartialOrder.rel top (ofProp p)

@[simp]

theorem Lean.Order.CompleteLattice.top_le_ofProp_iff {l : Type u_1} [CompleteLattice l] (p : Prop) : PartialOrder.rel top (ofProp p) ↔ p ∨ PartialOrder.rel top bot

theorem Lean.Order.CompleteLattice.le_ofProp {l : Type u_1} [CompleteLattice l] (x : l) (p : Prop) : p → PartialOrder.rel x (ofProp p)

x ⊑ ⌜p⌝ whenever p holds.

theorem Lean.Order.CompleteLattice.ofProp_le {l : Type u_1} [CompleteLattice l] (p : Prop) (rhs : l) : (p → PartialOrder.rel top rhs) → PartialOrder.rel (ofProp p) rhs

⌜p⌝ ⊑ rhs reduces to assuming p and proving ⊤ ⊑ rhs.

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

theorem Lean.Order.top_le_ofProp {l : Type u_1} [CompleteLattice l] (p : Prop) : p → PartialOrder.rel top (CompleteLattice.ofProp p)

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

theorem Lean.Order.le_ofProp {l : Type u_1} [CompleteLattice l] (x : l) (p : Prop) : p → PartialOrder.rel x (CompleteLattice.ofProp p)

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

theorem Lean.Order.ofProp_le {l : Type u_1} [CompleteLattice l] (p : Prop) (rhs : l) : (p → PartialOrder.rel top rhs) → PartialOrder.rel (CompleteLattice.ofProp p) rhs

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

theorem Lean.Order.CompleteLattice.ofProp_intro {l : Type u_1} [CompleteLattice l] (p : Prop) (h : l) : PartialOrder.rel (ofProp p) h = (p → PartialOrder.rel top h)

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

theorem Lean.Order.CompleteLattice.ofProp_intro_l {l : Type u_1} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet x (ofProp p)) y = (p → PartialOrder.rel x y)

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

theorem Lean.Order.CompleteLattice.ofProp_intro_r {l : Type u_1} [CompleteLattice l] (p : Prop) (x y : l) : PartialOrder.rel (meet (ofProp p) x) y = (p → PartialOrder.rel x y)

theorem Lean.Order.CompleteLattice.le_of_le_ofProp {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h1 : PartialOrder.rel Q (ofProp φ)) (h2 : φ → PartialOrder.rel Q R) : PartialOrder.rel Q R

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

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

theorem Lean.Order.CompleteLattice.ofProp_imp {l : Type u} [CompleteLattice l] (p₁ p₂ : Prop) : (p₁ → p₂) → PartialOrder.rel (ofProp p₁) (ofProp p₂)

theorem Lean.Order.CompleteLattice.ofProp_congr {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ofProp φ₁ = ofProp φ₂

theorem Lean.Order.CompleteLattice.ofProp_meet_le {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet (ofProp φ) Q) R

theorem Lean.Order.CompleteLattice.meet_ofProp_le {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet Q (ofProp φ)) R

theorem Lean.Order.CompleteLattice.ofProp_eq_top {l : Type u} [CompleteLattice l] {φ : Prop} (h : φ) : ofProp φ = top

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_meet_ofProp {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : meet (ofProp φ₁) (ofProp φ₂) = ofProp (φ₁ ∧ φ₂)

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_join_ofProp {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : join (ofProp φ₁) (ofProp φ₂) = ofProp (φ₁ ∨ φ₂)

theorem Lean.Order.CompleteLattice.ofProp_forall_le {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : PartialOrder.rel (ofProp (∀ (x : β), Φ x)) (iInf fun (x : β) => ofProp (Φ x))

@[simp]

theorem Lean.Order.CompleteLattice.iSup_ofProp {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : (iSup fun (x : β) => ofProp (Φ x)) = ofProp (∃ (x : β), Φ x)

@[simp]

theorem Lean.Order.CompleteLattice.iInf_ofProp {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : (iInf fun (x : β) => ofProp (Φ x)) = ofProp (∀ (x : β), Φ x)

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

theorem Lean.Order.ofProp_elim {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h1 : PartialOrder.rel Q (CompleteLattice.ofProp φ)) (h2 : φ → PartialOrder.rel Q R) : PartialOrder.rel Q R

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

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

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

theorem Lean.Order.ofProp_congr {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : CompleteLattice.ofProp φ₁ = CompleteLattice.ofProp φ₂

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

theorem Lean.Order.ofProp_meet_le {l : Type u} [CompleteLattice l] (p : Prop) (x rhs : l) : (p → PartialOrder.rel x rhs) → PartialOrder.rel (meet (CompleteLattice.ofProp p) x) rhs

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

theorem Lean.Order.ofProp_meet_le_left {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet (CompleteLattice.ofProp φ) Q) R

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

theorem Lean.Order.ofProp_meet_le_right {l : Type u} [CompleteLattice l] {Q R : l} {φ : Prop} (h : φ → PartialOrder.rel Q R) : PartialOrder.rel (meet Q (CompleteLattice.ofProp φ)) R

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

theorem Lean.Order.ofProp_eq_top {l : Type u} [CompleteLattice l] {φ : Prop} (h : φ) : CompleteLattice.ofProp φ = top

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

theorem Lean.Order.ofProp_and {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : meet (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂) = CompleteLattice.ofProp (φ₁ ∧ φ₂)

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

theorem Lean.Order.ofProp_or {l : Type u} [CompleteLattice l] {φ₁ φ₂ : Prop} : join (CompleteLattice.ofProp φ₁) (CompleteLattice.ofProp φ₂) = CompleteLattice.ofProp (φ₁ ∨ φ₂)

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

theorem Lean.Order.ofProp_forall_le {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : PartialOrder.rel (CompleteLattice.ofProp (∀ (x : β), Φ x)) (iInf fun (x : β) => CompleteLattice.ofProp (Φ x))

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

theorem Lean.Order.ofProp_exists {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : (iSup fun (x : β) => CompleteLattice.ofProp (Φ x)) = CompleteLattice.ofProp (∃ (x : β), Φ x)

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

theorem Lean.Order.ofProp_forall {l : Type u} [CompleteLattice l] {β : Sort u_1} {Φ : β → Prop} : (iInf fun (x : β) => CompleteLattice.ofProp (Φ x)) = CompleteLattice.ofProp (∀ (x : β), Φ x)

theorem Lean.Order.le_iSup_prop {l : Type u} [CompleteLattice l] (p : l) (a : Prop) (b : a → l) (ha : PartialOrder.rel p (CompleteLattice.ofProp a)) (hb : ∀ (h : a), PartialOrder.rel p (b h)) : PartialOrder.rel p (iSup fun (h : a) => b h)

theorem Lean.Order.le_apply_of_point_meet_le {σ : Type u} {β : Type v} [CompleteLattice β] (s : σ) (pre : β) (Q : σ → β) (h : PartialOrder.rel (fun (u : σ) => meet (CompleteLattice.ofProp (u = s)) pre) Q) : PartialOrder.rel pre (Q s)

theorem Lean.Order.point_meet_le_of_le_apply {σ : Type u} {β : Type v} [CompleteLattice β] (s : σ) (pre : β) (Q : σ → β) (h : PartialOrder.rel pre (Q s)) : PartialOrder.rel (fun (u : σ) => meet (CompleteLattice.ofProp (u = s)) pre) Q