map_comap_eq — Mathlib

English

For a semigroup hom f and a subsemigroup S of N, the image of the comapped S under f equals S intersected with the range of f.

Русский

Для полугомомера f и подполугруппы S ⊆ N, образ прообраза S через f равен пересечению S с образом f.

LaTeX

$$$(S.comap f).map f = S \cap f.srange$$

Lean4

@[to_additive]
theorem map_comap_eq (f : M →ₙ* N) (S : Subsemigroup N) : (S.comap f).map f = S ⊓ f.srange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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