map_comap_eq_self — Mathlib

English

For a map f and a submonoid S of N, the image of the comap of S along f equals the intersection S with the range of f, i.e., (S ∘ f) ∘ f = S ∩ Range(f).

Русский

Для отображения f и подмонoида S ⊆ N выполнено: image(comap f S) = S ∩ Range(f).

LaTeX

$$$ (S.\!comap f).map f = S \cap MonoidHom.mrange f $$$

Lean4

@[to_additive]
theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) : (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

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