iSup_comap_le — Mathlib

English

For a homomorphism f: G →* N and a family s(i) of Subgroups of N, ⨆ i, (s(i)).comap f ≤ (iSup s).comap f.

Русский

Для гомоморфизма f: G →* N и семейства подгрупп s(i) ⊆ N имеет: ⨆ i (s(i)).comap f ≤ (iSup s).comap f.

LaTeX

$$$\\bigl(\\bigcup_i s(i)\\bigr)^{\\mathrm{comap}\,f} \\le (\\bigcup_i s(i))^{\\mathrm{comap}\,f}$ (или в терминах iSup).$$

Lean4

@[to_additive]
theorem iSup_comap_le {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) : ⨆ i, (s i).comap f ≤ (iSup s).comap f :=
  Monotone.le_map_iSup fun _ _ => comap_mono

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