coe_mapLinearMap — Mathlib

English

The underlying function of the linear map mapLinearMap is exactly the original map F.map.

Русский

Фундаментальная функция линейного отображения mapLinearMap совпадает с исходным отображением F.map.

LaTeX

$$$\\forall X,Y\\,\\forall f:\\,X\\to Y:\\ $(F.mapLinearMap\\ R)\\,f = F.map\\,f$$$

Lean4

theorem coe_mapLinearMap {X Y : C} : ⇑(F.mapLinearMap R : (X ⟶ Y) →ₗ[R] _) = F.map :=
  rfl

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