coe — Mathlib

English

The coercion from continuous linear maps to linear maps is injective; two distinct continuous linear maps cannot have the same underlying linear map.

Русский

Встраивание из непрерывно линейного отображения в линейное отображение инъективно; два разных отображения не дают одинаковое линейное отображение.

LaTeX

$$The function $\\text{toLinearMap}$ is injective on $M_1 \\toSL[\\sigma] M_2$.$$

Lean4

/-- Coerce continuous linear maps to linear maps. -/
instance coe : Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) :=
  ⟨toLinearMap⟩

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