iSup_pow_of_ne_zero — Mathlib

English

For any nonempty index set, the supremum commutes with taking n-th powers when n ≠ 0.

Русский

Для ненулевого n и несократимого множества индексов верхний предел равен верхнему пределу f(i)^n.

LaTeX

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

Lean4

theorem iSup_pow_of_ne_zero (hn : n ≠ 0) (f : ι → ℝ≥0) : (⨆ i, f i) ^ n = ⨆ i, f i ^ n :=
  (NNReal.powOrderIso n hn).map_ciSup' _

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