mem_map_of_mem — Mathlib

English

If x lies in a substructure S of M, then its image f(x) lies in the image S.map f.

Русский

Если x принадлежит подструктуре S множества M, то его образ f(x) принадлежит образу S под отображением f.

LaTeX

$$$\\forall x \\in S,\; f(x) \\in S.map\\ f$$$

Lean4

theorem mem_map_of_mem (f : M →[L] N) {S : L.Substructure M} {x : M} (hx : x ∈ S) : f x ∈ S.map f :=
  mem_image_of_mem f hx

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