iInf_ne_top — Mathlib

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]

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