coeHom_injective — Mathlib

English

The forgetful map from the Schwartz space into the space of all functions is injective: different Schwartz maps yield different underlying functions.

Русский

Отображение, забывающее Schwartz-структуру, инъективно: различные SchwartzMap дают различные функции.

LaTeX

$$$\mathrm{coeHom}$ is injective$$

Lean4

theorem coeHom_injective : Function.Injective (coeHom E F) :=
  by
  rw [coe_coeHom]
  exact DFunLike.coe_injective

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