le_prod_iff — Mathlib

English

For H ≤ G, K ≤ N, and J ≤ G × N, J ≤ H.prod K if and only if the projections satisfy J mapped to G is ≤ H and J mapped to N is ≤ K.

Русский

Для H ≤ G, K ≤ N, и J ≤ G × N верно: J ≤ H.prod K тогда и только если соответствующие проекции удовлетворяют условию.

LaTeX

$$$ J \le H \mathrm{prod} K \iff \mathrm{map}(\mathrm{fst})\, J \le H \ \land\ \mathrm{map}(\mathrm{snd})\, J \le K $$$

Lean4

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

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