comap_map_comap — Mathlib

English

Similarly, applying comap then map then comap yields the original comap: ((S.comap f).map f).comap f = S.comap f.

Русский

Аналогично, повторение последовательности предобраза, отображения и предобраза возвращает исходный предобраз: ((S.comap f).map f).comap f = S.comap f.

LaTeX

$$$((\mathrm{comap}\!\_f\,S).\mathrm{map}\!\_f).\mathrm{comap}\!\_f = \mathrm{comap}\!\_f\,S$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_map_comap {S : Submonoid N} {f : F} : ((S.comap f).map f).comap f = S.comap f :=
  (gc_map_comap f).u_l_u_eq_u _

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