comp_toSpanSingleton — Mathlib

English

If f : M → N is linear and x ∈ M, then f ∘ toSpanSingleton x = toSpanSingleton (f x).

Русский

Если f линейно отображает M в N и x ∈ M, то композиция f с toSpanSingleton x равна toSpanSingleton (f x).

LaTeX

$$$f \circ_{\ell} toSpanSingleton\,R\,M\,x = toSpanSingleton\,R\,N\ (f x)$$$

Lean4

theorem comp_toSpanSingleton [AddCommMonoid M₂] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) :
    f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ (f x) := by ext; simp

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