apply_coe_mem_map — Mathlib

English

For a monoid homomorphism f and a submonoid S of M, the image of an element x ∈ S under f lies in the image submonoid S.map f.

Русский

Для моноидного гомоморфизма f и подмоноида S множества M образ x under f принадлежит образу S.map f.

LaTeX

$$$ f x \\in S.map f $ for any $x \\in S$$$

Lean4

@[to_additive]
theorem apply_coe_mem_map (f : F) (S : Submonoid M) (x : S) : f x ∈ S.map f :=
  mem_map_of_mem f x.2

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