comap_subtype_eq_top — Mathlib

English

The comap of p.subtype of p' equals top iff p is contained in p'.

Русский

Обратный образ (comap) по включению p.subtype от p' равен верхнему подмодулю тогда и только тогда, когда p ⊆ p'.

LaTeX

$$$$ \operatorname{comap}(p.\mathrm{subtype}, p') = \top \; \Longleftrightarrow \; p \subseteq p' $$$$

Lean4

@[simp]
theorem comap_subtype_eq_top {p p' : Submodule R M} : comap p.subtype p' = ⊤ ↔ p ≤ p' :=
  eq_top_iff.trans <| map_le_iff_le_comap.symm.trans <| by rw [map_subtype_top]

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