coe_apply — Mathlib

English

Applying the coerced continuous map to x yields the same value as applying the original function: (f : C(X,Y)) x = f x.

Русский

Применение приведённой непрерывной карты к точке x даёт то же самое, что и применение исходной функции: (f : C(X,Y)) x = f x.

LaTeX

$$$\\big( (f : C(X,Y)) \\big) x = f x$$$

Lean4

protected theorem coe_apply {F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) (x : X) :
    (f : C(X, Y)) x = f x :=
  rfl

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