csupr_ne_top — Mathlib

English

For SupSet α and f: ENNReal → α, the supremum over x ≠ ∞ equals the supremum over x ∈ ℝ≥0: ⨆ x (x ≠ ∞) f x = ⨆ x ∈ ℝ≥0 f x.

Русский

Для SupSet α и функции f: ENNReal → α, супермум по x ≠ ∞ равен супермуму по x ∈ ℝ≥0: ⨆ x (x ≠ ∞) f x = ⨆ x ∈ ℝ≥0 f x.

LaTeX

$$$ \sup_{x: x \neq \infty} f(x) = \sup_{x: x \in \mathbb{R}_{\ge 0}} f(x) $$$

Lean4

theorem csupr_ne_top [SupSet α] (f : ℝ≥0∞ → α) : ⨆ x : { x // x ≠ ∞ }, f x = ⨆ x : ℝ≥0, f x :=
  @cinfi_ne_top αᵒᵈ _ _

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