English
The coe (to linear map) from continuous linear maps to linear maps is injective; i.e., different continuous linear maps have different underlying linear maps.
Русский
Ощущение из непрерывно линейного отображения в линейное отображение инъективно; различные непрерывно линейные отображения имеют разные линейные части.
LaTeX
$$The map $\\text{toLinearMap}$ from $M_1 \\toSL[\\sigma] M_2$ to $M_1 \\to M_2$ is injective.$$
Lean4
/-- `ContinuousLinearMapClass F R M M₂` asserts `F` is a type of bundled continuous
`R`-linear maps `M → M₂`. This is an abbreviation for
`ContinuousSemilinearMapClass F (RingHom.id R) M M₂`. -/
abbrev ContinuousLinearMapClass (F : Type*) (R : outParam Type*) [Semiring R] (M : outParam Type*) [TopologicalSpace M]
[AddCommMonoid M] (M₂ : outParam Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂]
[FunLike F M M₂] :=
ContinuousSemilinearMapClass F (RingHom.id R) M M₂
