English
Goursat's lemma describes subgroups of a product: I is determined by appropriate subgroups of G and H and a normal isomorphism between quotients.
Русский
Лемма Гурсо описывает подгруппы произведения: I задаётся подходящими подгруппами G и H и нормальным изоморфизмом между частными группами.
LaTeX
$$$$\\exists (G' \\le G)\n\\exists (H' \\le H)\n\\exists (M \\lhd G') (N \\lhd H') (e: G'/M \\cong H'/N),\\; I = (\\text{graph}(e)^{\\,*}).$$$
Lean4
@[to_additive]
theorem normal_goursatSnd : I.goursatSnd.Normal :=
.map inferInstance _ hI₂