forall_ne_top — Mathlib

English

Let p be a predicate on ENNReal. Then p holds for every ENNReal value different from ∞ if and only if p holds for every finite ENNReal value.

Русский

Пусть p — предикат на ENNReal. Тогда p выполняется для каждого значения ENNReal, не равного ∞, тогда и только тогда, когда p выполняется для каждого конечного значения ENNReal.

LaTeX

$$$$ (\forall x:\\mathrm{ENNReal}, x \neq \\infty \Rightarrow p(x)) \\Longleftrightarrow \\left( \forall r:\\mathrm{NNReal}, p(r) \\right). $$$$

Lean4

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

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