map_comap_eq_self — Mathlib

English

If p ≤ range f, then map f (comap f p) = p (same as previous; reiteration).

Русский

Если 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_self [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂} (h : q ≤ range f) :
    map f (comap f q) = q := by rwa [Submodule.map_comap_eq, inf_eq_right]

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