to_from

Mathlib.Topology.Homotopy.HomotopyGroup

URI: https://scilib.ai/kg/mathlib#GenLoop.to_from

← MathLib Explorer

English

The composition toLoop i after fromLoop i is the identity on p.

Русский

Составление toLoop i ∘ fromLoop i есть тождественное по отношению к p.

LaTeX

$$toLoop i (fromLoop i p) = p$$

Lean4

theorem to_from (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : toLoop i (fromLoop i p) = p :=
  by
  simp_rw [toLoop, fromLoop, ContinuousMap.comp_assoc, toContinuousMap_comp_symm, ContinuousMap.comp_id]
  ext; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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