comap_injective — Mathlib

English

If f: G → N is surjective, then the map that sends a subgroup of N to its preimage under f is injective; i.e., K = L whenever f^{-1}(K) = f^{-1}(L).

Русский

Если f: G → N сюръективен, то отображение подгрупп N в их обратные прообраза по f инъективно: если f^{-1}(K) = f^{-1}(L), тогда K = L.

LaTeX

$$$\\text{Surj}(f) \\Rightarrow (K^{-1} = L^{-1} \\Rightarrow K=L)$$$

Lean4

@[to_additive]
theorem comap_injective {f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f) := fun K L => by
  simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

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