mkD_apply_of_continuous

Mathlib.Topology.ContinuousMap.ContinuousMapZero

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

← MathLib Explorer

English

If f is continuous and f(0) = 0, then the value of mkD f g at a point x is just f(x).

Русский

Если f непрерывна и f(0) = 0, то значение mkD f g в точке x равно f(x).

LaTeX

$$mkD(f,g)(x) = f(x)$$

Lean4

theorem mkD_apply_of_continuous [Zero X] {f : X → R} {g : C(X, R)₀} {x : X} (hf : Continuous f) (hf₀ : f 0 = 0) :
    mkD f g x = f x := by rw [mkD_of_continuous hf hf₀, coe_mk, ContinuousMap.coe_mk]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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