toLinearMap_toSpanSingleton — Mathlib

English

Composing a map with the span embedding equals the span-embedding of the composed image.

Русский

Сочетание отображения c вложением образа через span эквивалентно вложению span образа от композиции.

LaTeX

$$$ f \circ (toSpanSingleton x) = toSpanSingleton (f x).$$$

Lean4

@[simp]
theorem toLinearMap_toSpanSingleton (x : M₁) : (toSpanSingleton R₁ x).toLinearMap = LinearMap.toSpanSingleton R₁ M₁ x :=
  rfl

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