toContinuousLinearMap₁_apply

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.toContinuousLinearMap₁_apply

English

The mkContinuous construction applied to x returns the original value f x.

Русский

Применение конструктора mkContinuous к x возвращает исходное значение f x.

LaTeX

$$$(f.mkContinuous C h) x = f x$$$

Lean4

@[simp]
theorem toContinuousLinearMap₁_apply (f : 𝕜 →ₗ[𝕜] E) (x) : f.toContinuousLinearMap₁ x = f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru