map_comap_subtype — Mathlib

English

For submodules p and p' of a module M, the image of comap along the subtype embedding equals the intersection p ∩ p'.

Русский

Для подмодулей p и p' модуля M образ отображения через включение равен пересечению p и p'.

LaTeX

$$$\\operatorname{map} p.\\operatorname{subtype}(\\operatorname{comap} p.\\operatorname{subtype} p') = p \\cap p'.$$$

Lean4

@[simp]
theorem map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p' :=
  ext fun x => ⟨by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨⟨_, h₁⟩, h₂, rfl⟩⟩

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