English
For a predicate p on Nonempty α, there is an equivalence: (Exists h, p h) ↔ (Exists a, p ⟨a⟩).
Русский
Для предиката p на Nonempty α существует эквивалентность: (Exists h, p h) ↔ (Exists a, p ⟨a⟩).
LaTeX
$$$ \forall {\alpha}, \forall {p : Nonempty(\alpha) \to \mathrm{Prop}}, \big( \exists h : Nonempty(\alpha), p(h) \big) \iff \exists a, p(\langle a \rangle) $$$
Lean4
@[simp]
theorem «exists» {α} {p : Nonempty α → Prop} : (∃ h : Nonempty α, p h) ↔ ∃ a, p ⟨a⟩ :=
Iff.intro (fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦
⟨⟨a⟩, h⟩
-- Note: we set low priority here, to ensure it is not applied before `exists_prop`
-- and `exists_const`.
