comap_lt_comap_of_surjective — Mathlib

English

If f: G → N is surjective, then K^{-1} ≤ L^{-1} <=> K ≤ L for subgroups K,L ≤ N.

Русский

Если f: G → N сюръективен, то для подгрупп K,L ≤ N выполняется K^{-1} ≤ L^{-1} <=> K ≤ L.

LaTeX

$$$K,L \\le N,\\; \\text{Surj}(f) \\Rightarrow K^{-1} \\le L^{-1} \\iff K \\le L$$$

Lean4

@[to_additive]
theorem comap_lt_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
    K.comap f < L.comap f ↔ K < L := by simp_rw [lt_iff_le_not_ge, comap_le_comap_of_surjective hf]

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