prod_le_iff — Mathlib

English

For H ≤ G, K ≤ N, J ≤ H.prod K iff the images of H and K in the product are contained in J.

Русский

Для H ≤ G, K ≤ N, J ≤ H.prod K эквивалентно тому, что отображения H и K в произведение вложены в J.

LaTeX

$$$ H.prod K \le J \iff \mathrm{map}(\mathrm{inl})\, H \le J \ \,\land\ \, \mathrm{map}(\mathrm{inr})\, K \le J $$$

Lean4

@[to_additive prod_le_iff]
theorem prod_le_iff {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
    H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J := by
  simpa only [← Subgroup.toSubmonoid_le] using Submonoid.prod_le_iff

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