English
For any [CompleteLattice] α and f: ENNReal → α, the infimum over x ≠ ∞ equals the infimum over x ∈ ℝ≥0: ⨅ x (x ≠ ∞) f x = ⨅ x ∈ ℝ≥0 f x.
Русский
Для любого полнопорядкового замыкания α и функции f: ENNReal → α, инфимум по x ≠ ∞ равен инфимуму по x ∈ ℝ≥0: ⨅ x (x ≠ ∞) f x = ⨅ x ∈ ℝ≥0 f x.
LaTeX
$$$ \inf_{x: x \neq \infty} f(x) = \inf_{x: x \in \mathbb{R}_{\ge 0}} f(x) $$$
Lean4
theorem iInf_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) : ⨅ (x) (_ : x ≠ ∞), f x = ⨅ x : ℝ≥0, f x := by
rw [iInf_subtype', cinfi_ne_top]