English
Let p be a predicate on EReal. Then there exists an x in EReal with p(x) if and only if p holds at ⊥ or p holds at ⊤ or there exists a real r with p applied to r embedded into EReal.
Русский
Пусть p — предикат над EReal. Тогда существует элемент x ∈ EReal с p(x) тогда и только тогда, когда p выполняется для ⊥ или для ⊤ или существует вещественное число r, для которого p(r_EReal).
LaTeX
$$$\exists x\, p(x) \iff p(\bot) \lor p(\top) \lor \exists r \in \mathbb{R}, p(r).$$$
Lean4
protected theorem «exists» {p : EReal → Prop} : (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r : ℝ, p r
where
mp := by rintro ⟨r, hr⟩; cases r <;> aesop
mpr := by rintro (h | h | ⟨r, hr⟩) <;> exact ⟨_, ‹_›⟩
