coe_toRealLinearMap — Mathlib

English

For a continuous additive hom f: E →+ F, the underlying function of the associated real-linear map f.toRealLinearMap hf is exactly f.

Русский

Для непрерывного аддитивного гомоморфизма f: E →+ F соответствующее непрерывно-реал-линейное отображение f.toRealLinearMap hf имеет ту же функцию: лежит в основе f.

LaTeX

$$$\\forall x \\in E,\\; (f^{\\mathbb{R}\\text{-lin}})(x)=f(x).$$$

Lean4

@[simp]
theorem coe_toRealLinearMap (f : E →+ F) (hf : Continuous f) : ⇑(f.toRealLinearMap hf) = f :=
  rfl

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