English
Let p be a predicate on EReal. Then p holds for all elements of EReal if and only if p holds at ⊥, at ⊤, and p holds for every real number when viewed as an element of EReal.
Русский
Пусть p — предикат на EReal. Тогда p выполняется для всех элементов EReal тогда и только тогда, когда p выполняется для ⊥, для ⊤ и для каждого вещественного числа, рассматриваемого как элемент EReal.
LaTeX
$$$\forall {p: \mathrm{EReal} \to \mathrm{Prop}},\ (\forall x:\mathrm{EReal}, p(x)) \iff p(\bot) \land p(\top) \land \forall r \in \mathbb{R}, p(r).$$$
Lean4
protected theorem «forall» {p : EReal → Prop} : (∀ r, p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ r : ℝ, p r
where
mp h := ⟨h _, h _, fun _ ↦ h _⟩
mpr h := EReal.rec h.1 h.2.2 h.2.1
