fromLoop_symm_toLoop

Mathlib.Topology.Homotopy.HomotopyGroup

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

English

The reverse of the i-loop F = toLoop i p, under fromLoop, equals the i-coordinate symmetry symmAt i p.

Русский

Обратная к петле i-го типа F = toLoop i p по fromLoop равна симметрии symmAt i p.

LaTeX

$$$\\mathrm{fromLoop}(i)(\\mathrm{toLoop}(i)p)^{\\mathrm{symm}} = \\mathrm{symmAt}(i,p)$$$

Lean4

theorem fromLoop_symm_toLoop {i : N} {p : Ω^ N X x} : fromLoop i (toLoop i p).symm = symmAt i p :=
  (copy_eq _ _).symm

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

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

Разделы

Аффилиация

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