comp_toSpanSingleton — Mathlib

English

If f is nonzero and maps into a range, the range of f.smulRight x is the span of x.

Русский

Если f не нулевой и отображает в образ, то образ f.smulRight x равен диапазону x.

LaTeX

$$$\operatorname{range}(f.\text{smulRight} x) = \operatorname{span} \{ x \}.$$$

Lean4

theorem comp_toSpanSingleton (f : M₁ →L[R₁] M₂) (x : M₁) : f ∘L toSpanSingleton R₁ x = toSpanSingleton R₁ (f x) :=
  coe_inj.mp <| LinearMap.comp_toSpanSingleton _ _

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