coe_comap — Mathlib

English

For a Subsemigroup S of N and a multiplicative homomorphism f: M →* N, the set underlying the comap of S along f equals the preimage of S under f.

Русский

Для подполугруппы S ⊆ N и мультипликативного гомоморфизма f: M →* N множество подлежащего компа S вдоль f равно предобразу S по f.

LaTeX

$$$(S.comap f : \\text{Set } M) = f^{-1}' S$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_comap (S : Subsemigroup N) (f : M →ₙ* N) : (S.comap f : Set M) = f ⁻¹' S :=
  rfl

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