continuousMapClass

Mathlib.Topology.Path

URI: https://scilib.ai/kg/mathlib#Path.continuousMapClass

English

The underlying function of the path mk f h1 h2 equals f when f is a continuous map from I to X.

Русский

Пусть f: I → X непрерывно; опорная функция mk f h1 h2 имеет то же отображение как f.

LaTeX

$$$\big( (mk\, f\, h_1\, h_2) : Path x y \big)^{\!\,I \to X} = f$$$

Lean4

instance continuousMapClass : ContinuousMapClass (Path x y) I X where
  map_continuous γ := show Continuous γ.toContinuousMap by fun_prop

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

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

Разделы

Аффилиация

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