English
If a pair of subgroups forms a complementary pair in the sense of IsComplement', then they are disjoint and generate the full group.
Русский
Если пара подгрупп образует комплемент согласно IsComplement', то они не пересекаются и порождают всю группу.
LaTeX
$$IsComplement' H K induces IsCompl H K; i.e., Disjoint H K and H ⊔ K = ⊤.$$
Lean4
theorem isCompl (h : IsComplement' H K) : IsCompl H K :=
by
refine
⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
let x : H × K := ⟨⟨g, p⟩, 1⟩
let y : H × K := ⟨1, g, q⟩
Subtype.ext_iff.mp (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
codisjoint_iff_le_sup.mpr fun g _ => ?_⟩
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g
exact Subgroup.mul_mem_sup h.2 k.2
