refl

Mathlib.Topology.Homotopy.Path

URI: https://scilib.ai/kg/mathlib#Path.Homotopic.refl

English

For any path p, p is homotopic to itself.

Русский

Для каждого пути p существует гомотопия p к p.

LaTeX

$$$\forall p : Path x_0 x_1, \; p.Homotopic p$$$

Lean4

@[refl]
theorem refl (p : Path x₀ x₁) : p.Homotopic p :=
  ⟨Homotopy.refl p⟩

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

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

Разделы

Аффилиация

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