comap_equiv_eq_map_symm — Mathlib

English

Let f be a multiplicative equivalence between N and M and K a submonoid of M. Then the comap of K along f equals the image of K under the inverse equivalence: K.comap f = K.map f.symm.

Русский

Пусть f — моноидная эквиваленция между N и M, и K — подмономойд M. Тогда прообраз K по f равен образу K под обратной эквивалентностью: K.comap f = K.map f.symm.

LaTeX

$$$$ K.{comap}\,f = K.{map}\,f^{-1} $$$$

Lean4

@[to_additive]
theorem comap_equiv_eq_map_symm (f : N ≃* M) (K : Submonoid M) : K.comap f = K.map f.symm :=
  (map_equiv_eq_comap_symm f.symm K).symm

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