mkD_apply_of_continuous

Mathlib.Topology.ContinuousMap.Basic

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

English

If f is continuous, mkD f g applied to x equals f x.

Русский

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

LaTeX

$$$\text{mkD}(f,g)\,x = f\,x$$$

Lean4

theorem mkD_apply_of_continuous {f : α → β} {g : C(α, β)} {x : α} (hf : Continuous f) : mkD f g x = f x := by
  rw [mkD_of_continuous hf, coe_mk]

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

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

Разделы

Аффилиация

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