con_mono — Mathlib

English

If N ≤ M for normal subgroups N,M, then QuotientGroup.con N ≤ QuotientGroup.con M.

Русский

Если N ≤ M для нормальных подгрупп, то QuotientGroup.con N ≤ QuotientGroup.con M.

LaTeX

$$Con.instLE.le (QuotientGroup.con N) (QuotientGroup.con M)$$

Lean4

@[to_additive (attr := gcongr)]
theorem con_mono {N M : Subgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) :
    QuotientGroup.con N ≤ QuotientGroup.con M :=
  con_le_iff.mpr h

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