isCoatom_map_of_ker_le — Mathlib

English

If ker f ≤ p and p is a coatom, then map f p is a coatom.

Русский

Если ker f ⊆ p и p коатом, то map f p является коатомом.

LaTeX

$$$(\ker f \le p) \land IsCoatom(p) \Rightarrow IsCoatom(\operatorname{map}_f p)$$$

Lean4

theorem isCoatom_map_of_ker_le {f : F} (hf : Surjective f) {p : Submodule R M} (le : LinearMap.ker f ≤ p)
    (hp : IsCoatom p) : IsCoatom (map f p) :=
  (isCoatom_comap_iff hf).mp <| by rwa [comap_map_eq_self le]

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