apply_coe_mem_map

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.apply_coe_mem_map

English

If x is an element of S (viewed as a subset of M), then f x lies in S.map f.

Русский

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

LaTeX

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

Lean4

theorem apply_coe_mem_map (f : M →[L] N) (S : L.Substructure M) (x : S) : f x ∈ S.map f :=
  mem_map_of_mem f x.prop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru