mem_comap

Mathlib.Algebra.Module.Submodule.Map

URI: https://scilib.ai/kg/mathlib#Submodule.mem_comap

English

For injective f, the forward component of the equivalence maps x ∈ p to f(x).

Русский

При инъективном f первый компонент эквивалентности отображает x ∈ p в f(x).

LaTeX

$$f x ∈ map f p for x ∈ p$$

Lean4

@[simp]
theorem mem_comap {f : F} {p : Submodule R₂ M₂} : x ∈ comap f p ↔ f x ∈ p :=
  Iff.rfl

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

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

Разделы

Аффилиация

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