ofUnits_iSup — Mathlib

English

The ofUnits of the supremum over an index set equals the supremum of the ofUnits of the indexed subgroups.

Русский

Операция ofUnits сохраняет произвольную iSup: (iSup f).ofUnits = iSup (f i).ofUnits.

LaTeX

$$$\\bigl( iSup f \\bigr)^{\\mathrm{ofUnits}} = \\bigsup_{i} (f(i)^{\\mathrm{ofUnits}})$$$

Lean4

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

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