map_lt_map_of_le_of_sup_lt_sup — Mathlib

English

If p ≤ p' and p ⊔ ker f < p' ⊔ ker f, then map f p < map f p'.

Русский

Если p ⊆ p' и p ⊔ ker f < p' ⊔ ker f, то map f p < map f p'.

LaTeX

$$$p \le p' \land p \;⊔\; \ker f < p' \;⊔\; \ker f \Rightarrow \operatorname{map}_f p < \operatorname{map}_f p'$$$

Lean4

theorem map_lt_map_of_le_of_sup_lt_sup {p p' : Submodule R M} {f : F} (hab : p ≤ p')
    (h : p ⊔ LinearMap.ker f < p' ⊔ LinearMap.ker f) : Submodule.map f p < Submodule.map f p' :=
  by
  simp_rw [← comap_map_eq] at h
  exact lt_of_le_of_ne (map_mono hab) (ne_of_apply_ne _ h.ne)

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