English
Let A, A′, B be subgroups of a group G with A ≤ B and A′ ≤ B. Then the subgroup of B generated by A and A′ equals the join of the subgroups of B coming from A and from A′; equivalently (A ⊔ A′).subgroupOf B = A.subgroupOf B ⊔ A′.subgroupOf B.
Русский
Пусть A, A′, B — подгруппы группы G, причём A ≤ B и A′ ≤ B. Тогда подгруппа B, образованная порождающими A и A′, равна объединению соответствующих подгрупп B, полученных от A и A′; то есть (A ⊔ A′).subgroupOf B = A.subgroupOf B ⊔ A′.subgroupOf B.
LaTeX
$$$$(A \\sqcup A').subgroupOf B = A.subgroupOf B \\;\\sqcup\\; A'.subgroupOf B$$$$
Lean4
@[to_additive]
theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
(A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B :=
by
refine map_injective_of_ker_le B.subtype (ker_le_comap _ _) (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
