iSup_pow — Mathlib

English

For ENNReal, with nonempty index, supremum commutes with nth powers when n ≠ 0.

Русский

Для ENNReal непустого множества индексов суперпоследовательное максимальное значение совместимо со степенью n ≠ 0.

LaTeX

$$⨆ i, f i)^n = ⨆ i, f i^n for n ≠ 0$$

Lean4

theorem iSup_pow [Nonempty ι] (f : ι → ℝ≥0∞) (n : ℕ) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n :=
  by
  by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _

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