goursatFst_prod_goursatSnd_le — Mathlib

English

For a subgroup I of G × H with projections onto G and H surjective, the product of the projected normal subgroups I.goursatFst and I.goursatSnd lies inside I.

Русский

Для подгруппы I ⊆ G × H с сюръективными проекциями на G и H выполняется: I.goursatFst .prod I.goursatSnd ≤ I.

LaTeX

$$$ I.goursatFst.prod I.goursatSnd \\le I $$$

Lean4

@[to_additive AddSubgroup.goursatFst_prod_goursatSnd_le]
theorem goursatFst_prod_goursatSnd_le : I.goursatFst.prod I.goursatSnd ≤ I :=
  by
  rintro ⟨g, h⟩ ⟨hg, hh⟩
  simpa using mul_mem (mem_goursatFst.1 hg) (mem_goursatSnd.1 hh)

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