map_comap_eq_of_surjective — Mathlib

English

If f is surjective, then for any subsemigroup S of N, the image of its comap back to M recovers S: (S.comap f).map f = S.

Русский

Пусть f сюръективно отображает M на N. Тогда для любого подполугруппы S ⊆ N выполняется (S.comap f).map f = S.

LaTeX

$$$\\operatorname{Surjective}(f) \\rightarrow (S \\mathbin{.}\\operatorname{comap} f)\\mapsto f = S$$$

Lean4

@[to_additive]
theorem map_comap_eq_of_surjective (S : Subsemigroup N) : (S.comap f).map f = S :=
  (giMapComap hf).l_u_eq _

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