con_le_iff — Mathlib

English

For normal subgroups N,M of G, QuotientGroup.con N ≤ QuotientGroup.con M iff N ≤ M.

Русский

Для нормальных подгрупп N, M в G верно: QuotientGroup.con N ≤ QuotientGroup.con M тогда и только тогда, когда N ≤ M.

LaTeX

$$QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M$$

Lean4

@[to_additive (attr := simp)]
theorem con_le_iff {N M : Subgroup G} [N.Normal] [M.Normal] : QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M :=
  (Subgroup.orderIsoCon.map_rel_iff (a := ⟨N, inferInstance⟩) (b := ⟨M, inferInstance⟩))

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