X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
inst✝ : Nonempty Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
inhabit Y
no goals
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
inst✝ : Nonempty Y
inhabited_h : Inhabited Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
  fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩ <;> simp