attachBound_apply_coe — Mathlib

English

Evaluation of attachBound at a point recovers the original function value: the real-valued projection of (attachBound f)(x) equals f(x).

Русский

Значение attachBound в точке восстанавливает исходное значение функции: проекция на вещественные значения равна f(x).

LaTeX

$$$\big((\mathrm{attachBound} f)(x)\big)_{\mathbb{R}} = f(x)$$$

Lean4

@[simp]
theorem attachBound_apply_coe (f : C(X, ℝ)) (x : X) : ((attachBound f) x : ℝ) = f x :=
  rfl

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