toENNReal_lt_top — Mathlib

English

An ENNReal image is strictly less than the top element if and only if the original ENat is strictly less than top.

Русский

Образ в ENNReal строго меньше верхнего элемента тогда и только тогда, когда исходное ENat строго меньше верхнего.

LaTeX

$$$(n : \\mathbb{R}_{\\ge 0,\\infty}) < \\infty \\iff n < \\top.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_lt_top : (n : ℝ≥0∞) < ∞ ↔ n < ⊤ := by simp [← toENNReal_lt]

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