comap_injective_of_surjective — Mathlib

English

If f is surjective, the comap operation is injective: different subsemigroups of N yield different comaps in M.

Русский

Если f сюръективно, операция comap инъективна: различные подполугруппы N дают разные comap в M.

LaTeX

$$$\\operatorname{Surjective}(f) \\rightarrow \\operatorname{Injective}(\\operatorname{comap} f)$$$

Lean4

@[to_additive]
theorem comap_injective_of_surjective : Function.Injective (comap f) :=
  (giMapComap hf).u_injective

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