exists_ne_top — Mathlib

English

Let p be a predicate on ENNReal. There exists x ≠ ∞ with p x if and only if there exists r ≥ 0 with p (ofNNReal r).

Русский

Пусть p — предикат на ENNReal. Существует x ≠ ∞ such, что p(x), тогда существует r ≥ 0, такое что p(ofNNReal(r)).

LaTeX

$$$$ (\exists x:\\mathrm{ENNReal}, x \neq \\infty \land p(x)) \iff \exists r:\\mathrm{NNReal}, p(r). $$$$

Lean4

theorem exists_ne_top {p : ℝ≥0∞ → Prop} : (∃ x ≠ ∞, p x) ↔ ∃ x : ℝ≥0, p x :=
  WithTop.exists_ne_top

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