instCoeToLinearMap — Mathlib

English

There is a canonical coercion from F to the type of positive linear maps given by f ↦ toPositiveLinearMap(f).

Русский

Существует каноническое приведение из F к типу положительных линейных отображений, задаваемое f ↦ toPositiveLinearMap(f).

LaTeX

$$$\\operatorname{coe}_{F \\to \\mathrm{Pos}}\;: F \\to (E_1 \\to_{R}^{+} E_2)$$$

Lean4

/-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/
instance instCoeToLinearMap : CoeHead F (E₁ →ₚ[R] E₂) where coe f := toPositiveLinearMap f

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