noncommPiCoprod_range — Mathlib

English

The image of the canonical homomorphism from the commuting family of subgroups equals the join (supremum) of the subgroups H_i, i.e., the subgroup generated by all H_i.

Русский

Образ канонического гомоморфизма из коммутирующего семейства подгрупп равен наибольшему нижнему пределу этих подгрупп, то есть подгруппе, созданной порождением всех H_i.

LaTeX

$$$\operatorname{range}(\text{noncommPiCoprod } hcomm) = \bigvee_{i\in \iota} H_i$$$

Lean4

@[to_additive]
theorem noncommPiCoprod_range {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} :
    (noncommPiCoprod hcomm).range = ⨆ i : ι, H i := by simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]

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