coe_mk

Mathlib.Topology.ContinuousMap.ContinuousMapZero

URI: https://scilib.ai/kg/mathlib#ContinuousMapZero.coe_mk

English

For any f ∈ C(X,R) and h0 with f(0)=0, the element mk f h0, when viewed as a function X → R, equals f.

Русский

Для любого f ∈ C(X,R) и h0 с условием f(0)=0 элемент mk f h0, при рассмотрении как функция X → R, равен f.

LaTeX

$$$\\mathrm{coe}(\\mathrm{mk}\\, f\\, h_0) = f$$$

Lean4

@[simp]
theorem coe_mk {f : C(X, R)} {h0 : f 0 = 0} : ⇑(mk f h0) = f :=
  rfl

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

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

Разделы

Аффилиация

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