toFun_eq_coe

Mathlib.Topology.ContinuousMap.Defs

URI: https://scilib.ai/kg/mathlib#ContinuousMap.toFun_eq_coe

English

For any f ∈ C(X,Y) (or F with FunLike), the internal function part equals the coercion to X→Y: f.toFun = (f : X → Y).

Русский

У любого отображения f∈C(X,Y) функция внутри равно приведению к X→Y: f.toFun = (f : X→Y).

LaTeX

$$$f.toFun = (f : X \\to Y)$$$

Lean4

@[simp]
theorem toFun_eq_coe {f : C(X, Y)} : f.toFun = (f : X → Y) :=
  rfl

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

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

Разделы

Аффилиация

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