Theorem: isPathConnected_multibrotExt (Ray/Dynamics/Multibrot/Connected.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (multibrotExt d)
Tactic:
rw [← ray_surj d]
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ray d '' ball 0 1)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ray d '' ball 0 1)
Tactic:
apply IsPathConnected.image_of_continuousOn
State after:
case sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ball 0 1)

case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)

State before:
case sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ball 0 1)

case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Tactic:
exact (convex_ball _ _).isPathConnected (Metric.nonempty_ball.mpr one_pos)
State after:
case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)

State before:
case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Tactic:
exact (rayHolomorphic d).continuousOn
State after:
no goals