instSubsingletonPUnitUnit

Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit

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

English

There is at most one path from PUnit.unit to PUnit.unit, i.e., the path space is a singleton.

Русский

От путей от PUnit.unit к PUnit.unit не более одной, т.е. пространство путей является единичным.

LaTeX

$$$$ \\forall p,q:\\, Path(PUnit.unit, PUnit.unit),\\ p=q. $$$$

Lean4

instance : Subsingleton (Path PUnit.unit PUnit.unit) :=
  ⟨fun x y => by ext⟩

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

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

Разделы

Аффилиация

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