comap_lt_of_lt_map_of_injective — Mathlib

English

If q < p.map f then q.comap f < p.

Русский

Если q меньше образа p под действием f, то обратный образ q меньше p.

LaTeX

$$$\forall p:\, Submodule\; R\; M,\forall q:\, Submodule\; R_2\; M_2,\ q < p.map f \Rightarrow q.comap f < p$$$

Lean4

theorem comap_lt_of_lt_map_of_injective {p : Submodule R M} {q : Submodule R₂ M₂} (h : q < p.map f) : q.comap f < p :=
  by
  rw [← map_lt_map_iff_of_injective hf]
  exact (map_comap_le _ _).trans_lt h

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