map_comap_eq — Mathlib

English

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

Русский

Если p ⊆ range f, то map f (comap f p) = p.

LaTeX

$$$p \le \operatorname{range} f \;\Rightarrow\; \operatorname{map} f (\operatorname{comap} f p) = p$$$

Lean4

theorem _root_.Submodule.map_comap_eq [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) :
    map f (comap f q) = range f ⊓ q :=
  le_antisymm (le_inf map_le_range (map_comap_le _ _)) <| by rintro _ ⟨⟨x, _, rfl⟩, hx⟩; exact ⟨x, hx, rfl⟩

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