English
If p and q are homotopic, then their i-th loops are homotopic for any i.
Русский
Если p и q гомотопны, то их i-й петли гомотопны.
LaTeX
$$$ \\forall i:\\,N,\\; \\forall p,q:\\,\\Omega^N X x,\\; Homotopic p q \\to (toLoop\,i\,p) \\ Homotopic (toLoop\,i\,q)$$$
Lean4
theorem homotopicTo (i : N) {p q : Ω^ N X x} : Homotopic p q → (toLoop i p).Homotopic (toLoop i q) :=
by
refine Nonempty.map fun H => ⟨⟨⟨fun t => ⟨homotopyTo i H t, ?_⟩, ?_⟩, ?_, ?_⟩, ?_⟩
· rintro y ⟨i, iH⟩
rw [homotopyTo_apply, H.eq_fst, p.2]
all_goals apply Cube.insertAt_boundary; right; exact ⟨i, iH⟩
· fun_prop
iterate 2
intro
ext
dsimp
rw [homotopyTo_apply, toLoop_apply]
swap
· apply H.apply_zero
· apply H.apply_one
intro t y yH
ext
dsimp
rw [homotopyTo_apply]
apply H.eq_fst; use i
rw [funSplitAt_symm_apply, dif_pos rfl]; exact yH
