prod_mono — Mathlib

English

If H ≤ H' in G and K ≤ K' in N, then H × K ≤ H' × K' as subgroups of G × N.

Русский

Если H ≤ H' в G и K ≤ K' в N, то H × K ≤ H' × K' как подгруппы G × N.

LaTeX

$$$ H \le H' \Rightarrow K \le K' \Rightarrow H \mathrm{prod} K \le H' \mathrm{prod} K' $$$

Lean4

@[to_additive prod_mono]
theorem prod_mono : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) (@prod G _ N _) (@prod G _ N _) := fun _s _s' hs _t _t' ht =>
  Set.prod_mono hs ht

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