iSup₂_pow_of_ne_zero — Mathlib

English

For a two-index function f(i,j), the double supremum raised to n equals the double supremum of powers: (⨆ i ⨆ j f i j)^n = ⨆ i ⨆ j f i j ^ n for n ≠ 0.

Русский

Для двойной функции f(i,j)ustre верхняя двойная граница возводится в степень n ≠ 0 одинаково с двойной степенью по каждому аргументу.

LaTeX

$$(⨆ i, ⨆ j, f(i,j))^n = ⨆ i, ⨆ j, f(i,j)^n \quad (n ≠ 0)$$

Lean4

theorem iSup₂_pow_of_ne_zero {κ : ι → Sort*} (f : (i : ι) → κ i → ℝ≥0∞) {n : ℕ} (hn : n ≠ 0) :
    (⨆ i, ⨆ j, f i j) ^ n = ⨆ i, ⨆ j, f i j ^ n :=
  (powOrderIso n hn).map_iSup₂ f

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