exists_const_iff — Mathlib

English

Let α be a type and P a proposition. (Exists x : α, P) holds iff (Nonempty α) and P hold.

Русский

Пусть α — тип и P — proposition. Существует x : α, P эквивалентно тому, что α непусто и P верно.

LaTeX

$$$ \exists x : \alpha, P \iff (\operatorname{Nonempty}(\alpha) \land P) $$$

Lean4

@[simp low]
theorem exists_const_iff {α : Sort*} {P : Prop} : (∃ _ : α, P) ↔ Nonempty α ∧ P :=
  Iff.intro (fun ⟨a, h⟩ ↦ ⟨⟨a⟩, h⟩) fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩

Похожие утверждения