X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x a b : X
⊢ Homotopic (↑genLoopZeroEquiv.symm a).toContinuousMap (↑genLoopZeroEquiv.symm b).toContinuousMap ↔ Joined a b
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x a b : X
⊢ GenLoop.Homotopic (↑genLoopZeroEquiv.symm a) (↑genLoopZeroEquiv.symm b) ↔ Joined a b
rw [GenLoop.Homotopic, Cube.boundary_zero, homotopicRel_empty]
no goals
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x a b : X
⊢ Homotopic (↑genLoopZeroEquiv.symm a).toContinuousMap (↑genLoopZeroEquiv.symm b).toContinuousMap ↔ Joined a b
exact homotopic_const_iff