apply_coe_mem_map

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.apply_coe_mem_map

English

For f, I, and x ∈ I (as a member of the subtype), f x ∈ I.map f.

Русский

Для f, I и x ∈ I (как элемент подмножества), f x ∈ I.map f.

LaTeX

$$$f x \\in I.map f$ for $x \\in I$$$

Lean4

theorem apply_coe_mem_map (f : F) (I : Ideal R) (x : I) : f x ∈ I.map f :=
  mem_map_of_mem f x.2

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

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

Разделы

Аффилиация

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