map_le_iff_le_comap — Mathlib

English

For closed submodules s ⊆ M and t ⊆ N, we have map f s ≤ t if and only if s ≤ comap f t.

Русский

Для замкнутых подмодульов s ⊆ M и t ⊆ N выполняется: map f s ≤ t тогда и только тогда, когда s ≤ comap f t.

LaTeX

$$$ClosedSubmodule.map f s \le t \iff s \le ClosedSubmodule.comap f t$$$

Lean4

theorem map_le_iff_le_comap {s : ClosedSubmodule R M} {t : ClosedSubmodule R N} : map f s ≤ t ↔ s ≤ comap f t := by
  simp [map, Submodule.map_le_iff_le_comap]; simp [← toSubmodule_le_toSubmodule]

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