range_comp_of_range_eq_top — Mathlib

English

If range f = ⊤, then range (g ∘ f) = range g.

Русский

Если образ f равен ⊤, то образ (g ∘ f) равен образу g.

LaTeX

$$$$ \operatorname{range}(g \circ f) = \operatorname{range}(g) \quad\text{whenever } \operatorname{range} f = \top $$$$

Lean4

theorem range_comp_of_range_eq_top [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃]
    {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : range f = ⊤) : range (g.comp f : M →ₛₗ[τ₁₃] M₃) = range g := by
  rw [range_comp, hf, Submodule.map_top]

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