isCoatom_comap_or_eq_top — Mathlib

English

For any f, IsCoatom (comap f p) or comap f p equals the top element.

Русский

Для любого f либо comap f p является коатомом, либо comap f p равно верхушке.

LaTeX

$$$IsCoatom(\operatorname{comap}_f p) \lor \operatorname{comap}_f p = \top$$$

Lean4

theorem isCoatom_comap_or_eq_top (f : F) {p : Submodule R₂ M₂} (hp : IsCoatom p) :
    IsCoatom (comap f p) ∨ comap f p = ⊤ :=
  or_iff_not_imp_right.mpr fun h ↦
    ⟨h, fun q lt ↦ by
      rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]
      simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_ge⟩

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