toBoundedContinuousFunction_apply

English

The evaluation of the bounded continuous function associated to a Schwartz map at a point x is given by the map's value at x: toBoundedContinuousFunction_apply states f(x) = f x.

Русский

Значение ограниченной непрерывной функции, связанной с отображением Шварца, в точке x равно значению самого отображения в x.

LaTeX

$$$$ f^{\\mathrm{toBCF}}(x) = f(x). $$$$

Lean4

@[simp]
theorem toBoundedContinuousFunction_apply (f : 𝓢(E, F)) (x : E) : f.toBoundedContinuousFunction x = f x :=
  rfl

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