comap_subtype_le_iff — Mathlib

English

q.comap p.subtype ≤ r.comap p.subtype iff p ∩ q ≤ p ∩ r.

Русский

q.comap p.subtype ≤ r.comap p.subtype тогда и только тогда, когда p ∩ q ≤ p ∩ r.

LaTeX

$$$$ q.\mathrm{comap}(p.\mathrm{subtype}) \le r.\mathrm{comap}(p.\mathrm{subtype}) \iff p \cap q \le p \cap r $$$$

Lean4

@[simp]
theorem comap_subtype_le_iff {p q r : Submodule R M} : q.comap p.subtype ≤ r.comap p.subtype ↔ p ⊓ q ≤ p ⊓ r :=
  ⟨fun h ↦ by simpa using map_mono (f := p.subtype) h, fun h ↦ by simpa using comap_mono (f := p.subtype) h⟩

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