comap_le_comap_iff_of_surjective

Mathlib.Algebra.Module.Submodule.Map

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

English

For surjective f, p.comap f ≤ q.comap f if and only if p ≤ q.

Русский

При сюръективности f p.comap f ≤ q.comap f тогда и только тогда, когда p ≤ q.

LaTeX

$$$p \operatorname{comap} f \le q \operatorname{comap} f \;\iff\; p \le q$$$

Lean4

theorem comap_le_comap_iff_of_surjective {p q : Submodule R₂ M₂} : p.comap f ≤ q.comap f ↔ p ≤ q :=
  (giMapComap hf).u_le_u_iff

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

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

Разделы

Аффилиация

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