ofUnits_sSup — Mathlib

English

The ofUnits of the supremum over a set of subgroups of Units M equals the supremum of their respective ofUnits.

Русский

Над множеством подгрупп единиц M действует равенство: (sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits.

LaTeX

$$$(sSup\\, s)^{\\mathrm{ofUnits}} = \\bigsqcup_{S\\in s} S^{\\mathrm{ofUnits}}$$

Lean4

@[to_additive]
theorem ofUnits_sSup (s : Set (Subgroup Mˣ)) : (sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits :=
  ofUnits_units_gc.l_sSup

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