range_comp_le_range — Mathlib

English

For linear maps f and g, range(g ∘ f) = map g (range f).

Русский

Для линейных отображений f и g, образ композиции равен образу g от образа f.

LaTeX

$$$\operatorname{range}(g \circ f) = \operatorname{map} g (\operatorname{range} f)$$$

Lean4

theorem range_comp_le_range [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    range (g.comp f : M →ₛₗ[τ₁₃] M₃) ≤ range g :=
  SetLike.coe_mono (Set.range_comp_subset_range f g)

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