English
If the quotient by a subgroup is a singleton, then the subgroup must be the whole group.
Русский
Если фактор-группа по подгруппе является одиночной, то подгруппа равна всей группе.
LaTeX
$$$\\text{Subsingleton}(G\\!/H) \\Rightarrow H = G$$$
Lean4
/-- The **correspondence theorem**, or lattice theorem,
or fourth isomorphism theorem for multiplicative groups -/
@[to_additive /-- The **correspondence theorem**, or lattice theorem,
or fourth isomorphism theorem for additive groups -/
]
def comapMk'OrderIso (N : Subgroup G) [hn : N.Normal] : Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H }
where
toFun H' := ⟨Subgroup.comap (mk' N) H', le_comap_mk' N _⟩
invFun H := Subgroup.map (mk' N) H
left_inv H' := Subgroup.map_comap_eq_self <| by simp
right_inv := fun ⟨H, hH⟩ => Subtype.ext <| by simpa
map_rel_iff' := Subgroup.comap_le_comap_of_surjective <| mk'_surjective _
