iSup_pow — Mathlib

English

For Real-valued f with f(i) ≥ 0, and nonzero n, the supremum commutes with nth powers under embedding to NNReal.

Русский

Для f(i) ≥ 0 на i и n ≠ 0, sup f(i)^n равно sup (f(i))^n.

LaTeX

$$If f: i → Real with f(i) ≥ 0 and n ≠ 0 then (⨆ i f(i))^n = ⨆ i f(i)^n$$

Lean4

theorem iSup_pow [Nonempty ι] {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n := by
  lift f to ι → ℝ≥0 using hf; dsimp; exact mod_cast NNReal.iSup_pow f n

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