mem_map_of_mem

Mathlib.Algebra.Lie.Submodule

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

English

If m belongs to N, then its image f(m) belongs to N.map f.

Русский

Если m принадлежит N, то образ f(m) принадлежит N.map f.

LaTeX

$$$ m \in N \implies f m \in N.map f $$$

Lean4

theorem mem_map_of_mem {m : M} (h : m ∈ N) : f m ∈ N.map f :=
  Set.mem_image_of_mem _ h

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

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

Разделы

Аффилиация

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