coe_toContinuousLinearMap — Mathlib

English

The underlying function of the continuous linear map associated to a linear isometry equals the original isometry function.

Русский

Базовая функция непрерывного линейного отображения, связанного с линейной изометрией, совпадает с исходной функцией изометрии.

LaTeX

$$∀x, (toContinuousLinearMap(f))(x) = f(x)$$

Lean4

@[simp]
theorem coe_toContinuousLinearMap : ⇑f.toContinuousLinearMap = f :=
  rfl

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