forall_ennreal — Mathlib

English

Let P be a predicate on ENNReal. Then P holds for every ENNReal if and only if P holds for all finite ENNReal values and P holds at infinity.

Русский

Пусть P — предикат на ENNReal. Тогда P выполняется для каждого элемента ENNReal тогда и только тогда, когда P выполняется для всех конечных значений ENNReal и P выполняется в бесконечности.

LaTeX

$$$$ (\forall a:\\mathrm{ENNReal},\ p(a)) \\Longleftrightarrow \\left( \forall r:\\mathrm{NNReal},\ p(r) \\right) \land p(\\infty) $$$$

Lean4

theorem forall_ennreal {p : ℝ≥0∞ → Prop} : (∀ a, p a) ↔ (∀ r : ℝ≥0, p r) ∧ p ∞ :=
  WithTop.forall.trans and_comm

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