mem_map_of_mem

Mathlib.RingTheory.Ideal.Maps

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

English

If x ∈ I, then f(x) ∈ map f I.

Русский

Если x ∈ I, то f(x) ∈ map f I.

LaTeX

$$$x \\in I \\Rightarrow f(x) \\in \\mathrm{map} f I$$$

Lean4

theorem mem_map_of_mem (f : F) {I : Ideal R} {x : R} (h : x ∈ I) : f x ∈ map f I :=
  subset_span ⟨x, h, rfl⟩

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

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

Разделы

Аффилиация

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