Documentation

Std.Internal.Order.Prop

The lattice of propositions #

Lemmas at carrier Prop: ⊑ is implication, ⊓ is ∧, ⊔ is ∨, ⨅ is ∀, ⨆ is ∃, ⊤ is True, ⊥ is False, ⇨ is →, and ⌜p⌝ is p.

source
@[simp]
theorem Lean.Order.le_prop_eq_imp (p q : Prop) :
PartialOrder.rel p q = (p → q)
source
theorem Lean.Order.le_of_imp_top_le (x y : Prop) :
(x → PartialOrder.rel top y) → PartialOrder.rel x y
source
theorem Lean.Order.top_le_prop (x : Prop) :
x → PartialOrder.rel top x
source
theorem Lean.Order.le_prop_of_right (x y : Prop) :
y → PartialOrder.rel x y
source
theorem Lean.Order.of_top_le_prop {x : Prop} :
PartialOrder.rel top x → x
source
theorem Lean.Order.true_le_of_top_le (x : Prop) :
PartialOrder.rel top x → PartialOrder.rel True x
source
@[simp]
theorem Lean.Order.iInf_prop_eq_forall {ι : Type uₗ} (f : ι → Prop) :
iInf f = ∀ (i : ι), f i
source
theorem Lean.Order.le_forall {β : Sort uₗ} (p : Prop) (q : β → Prop) (h : ∀ (x : β), PartialOrder.rel p (q x)) :
PartialOrder.rel p (∀ (x : β), q x)

Introduction rule for a ∀ on the RHS of a Prop entailment.

source
theorem Lean.Order.le_and (p a b : Prop) (ha : PartialOrder.rel p a) (hb : PartialOrder.rel p b) :
PartialOrder.rel p (a ∧ b)
source
theorem Lean.Order.le_exists_prop (p a : Prop) (b : a → Prop) (ha : PartialOrder.rel p a) (hb : ∀ (h : a), PartialOrder.rel p (b h)) :
PartialOrder.rel p (∃ (h : a), b h)
source
@[simp]
theorem Lean.Order.iSup_prop_eq_exists {ι : Type uₗ} (f : ι → Prop) :
iSup f = ∃ (i : ι), f i
source
@[simp]
theorem Lean.Order.meet_prop_eq_and (a b : Prop) :
meet a b = (a ∧ b)
source
@[simp]
theorem Lean.Order.join_prop_eq_or (a b : Prop) :
join a b = (a ∨ b)
source
@[simp]
theorem Lean.Order.top_prop_eq :
top = True

The top element of the Prop lattice is True.

source
@[simp]
theorem Lean.Order.bot_prop_eq :
bot = False

The bottom element of the Prop lattice is False.

source
@[deprecated Lean.Order.le_prop_of_right (since := "2026-09-24")]
theorem Lean.Order.le_of_right (x y : Prop) :
y → PartialOrder.rel x y
source
@[simp]
theorem Lean.Order.CompleteLattice.ofProp_prop_eq (p : Prop) :
ofProp p = p

Embedding a proposition into the Prop lattice (⌜p⌝) is the proposition itself.

source
@[deprecated Lean.Order.CompleteLattice.ofProp_prop_eq (since := "2026-09-24")]
theorem Lean.Order.ofProp_prop_eq (p : Prop) :
CompleteLattice.ofProp p = p
source
@[simp]
theorem Lean.Order.himp_prop_eq_imp (a b : Prop) :
himp a b = (a → b)