coe_toContinuousMap

Mathlib.Topology.Path

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

English

Let γ be a path from x to y. When viewed as a continuous map I → X, γ coincides with its underlying path.

Русский

Пусть γ — путь от x до y. Рассматривая γ как непрерывную карту I → X, мы получаем ту же саму функцию, что и путь.

LaTeX

$$$ (\\operatorname{toContinuousMap}(\\gamma)) = γ $$$

Lean4

@[simp]
theorem coe_toContinuousMap : ⇑γ.toContinuousMap = γ :=
  rfl

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

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

Разделы

Аффилиация

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