map_iSup — Mathlib

English

For an index set I and subgroups s(i) ⊆ G, map of the iSup is the iSup of the maps: (iSup s).map f = iSup (s i).map f.

Русский

Для семейства подгрупп s(i) ⊆ G имеем (iSup s).map f = ⨆ i, (s(i)).map f.

LaTeX

$$$\\mathrm{map}_f\\bigl(\\bigl\\uparrow\\!\\! i\\mathrm{Sup}\\, s\\bigr) = \\bigvee_i (\\mathrm{map}_f (s(i))).$$$

Lean4

@[to_additive]
theorem map_iSup {ι : Sort*} (f : G →* N) (s : ι → Subgroup G) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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