map_comap_eq_self_of_surjective — Mathlib

English

If f is surjective, then map f (comap f S) = S for any submonoid S.

Русский

Если f сюръективно отображает, тогда map f (comap f S) = S для любого подмoного S.

LaTeX

$$$ map f (comap f S) = S $ when f is surjective$$

Lean4

@[to_additive]
theorem map_comap_eq_self_of_surjective {f : F} (h : Function.Surjective f) {S : Submonoid N} : map f (comap f S) = S :=
  map_comap_eq_self (MonoidHom.mrange_eq_top_of_surjective _ h ▸ le_top)

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