ofUnits_iSup₂ — Mathlib

English

The ofUnits of a double indexed supremum equals the double supremum of the ofUnits.

Русский

Операция ofUnits сохраняет двойную индексированную iSup: (iSup i j).ofUnits = iSup i j (f(i,j)).ofUnits.

LaTeX

$$$\\bigl( iSup_{i} \\; iSup_{j} f(i,j) \\bigr)^{\\mathrm{ofUnits}} = \\; iSup_{i} \\; iSup_{j} (f(i,j)^{\\mathrm{ofUnits}})$$$

Lean4

@[to_additive]
theorem ofUnits_iSup₂ {ι : Sort*} {κ : ι → Sort*} (f : (i : ι) → κ i → Subgroup Mˣ) :
    (⨆ (i : ι), ⨆ (j : κ i), f i j).ofUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofUnits :=
  ofUnits_units_gc.l_iSup₂

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