English
Let p be a predicate on NNReal. Then p holds for every NNReal if and only if p holds for every real x with x ≥ 0, when applied to the corresponding NNReal element ⟨x, hx⟩.
Русский
Пусть p — предикат на множество NNReal. Тогда для всех элементов NNReal выполняется p, если и только если для каждого действительного числа x, неотрицательного по смыслу, p выполняется для соответствующего элемента ⟨x, hx⟩.
LaTeX
$$$ (\forall p : \mathbb{R}_{\ge 0} \to \text{Prop})\;\Big( (\forall x : \mathbb{R}_{\ge 0}, p\,x) \;\leftrightarrow\; \forall (x : \mathbb{R}) (hx : 0 \le x), p \langle x, hx \rangle \Big) $$$
Lean4
protected theorem «forall» {p : ℝ≥0 → Prop} : (∀ x : ℝ≥0, p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩ :=
Subtype.forall
