map_comap_map — Mathlib

English

Applying map then comap then map returns the original mapped submonoid: ((S.map f).comap f).map f = S.map f.

Русский

Применение отображения, затем предобраза, затем отображения возвращает исходное отображение: ((S.map f).comap f).map f = S.map f.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem map_comap_map {f : F} : ((S.map f).comap f).map f = S.map f :=
  (gc_map_comap f).l_u_l_eq_l _

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