id_eq_path_refl

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

URI: https://scilib.ai/kg/mathlib#FundamentalGroupoid.id_eq_path_refl

English

The identity morphism in the fundamental groupoid is the path refl x.as.

Русский

Идентичный морфизм в фундаментальном групоиде — это путь refl x.as.

LaTeX

$$$$ \\mathrm{id}_{x} = \\llbracket \\mathrm{Path.refl}(x.as) \\rrbracket, $$$$

Lean4

theorem id_eq_path_refl (x : FundamentalGroupoid X) : 𝟙 x = ⟦Path.refl x.as⟧ :=
  rfl

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

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

Разделы

Аффилиация

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