comap_map_sup_of_comap_le — Mathlib

English

If comap f q ≤ p, then comap f (map f p ⊔ q) = p.

Русский

Если comap f q ≤ p, тогда comap f (map f p ⊔ q) = p.

LaTeX

$$$\operatorname{comap}_f(\operatorname{map}_f p \;⊔\; q) = p \quad\text{при } \operatorname{comap}_f q \le p$$$

Lean4

theorem comap_map_sup_of_comap_le {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} (le : comap f q ≤ p) :
    comap f (map f p ⊔ q) = p :=
  by
  refine le_antisymm (fun x h ↦ ?_) (map_le_iff_le_comap.mp le_sup_left)
  obtain ⟨_, ⟨y, hy, rfl⟩, z, hz, eq⟩ := mem_sup.mp h
  rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq
  simpa using p.add_mem (le hz) hy

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