Theorem: isPathConnected_sphere (Ray/Misc/Connected.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (sphere z r)
Tactic:
rw [← abs_of_nonneg r0, ← image_circleMap_Ioc z r]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (circleMap z r '' Ioc 0 (2 * π))

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (circleMap z r '' Ioc 0 (2 * π))
Tactic:
refine IsPathConnected.image ?_ (continuous_circleMap _ _)
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (Ioc 0 (2 * π))

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (Ioc 0 (2 * π))
Tactic:
exact (convex_Ioc 0 (2 * π)).isPathConnected (nonempty_Ioc.mpr Real.two_pi_pos)
State after:
no goals