6.34. MappingDegree.IsPathConnectedBallMinusCountable🔗

Jacobians.MappingDegree.IsPathConnectedBallMinusCountable — source

Set.Countable.isPathConnected_ball_diff_complex

Ball-restricted analogue of Set.Countable.isPathConnected_compl_of_one_lt_rank for the complex plane: the relative complement of a countable set inside an open ball of ℂ is path-connected.

theorem Set.Countable.isPathConnected_ball_diff_complex
    {z : ℂ} {r : ℝ} (hr : 0 < r) {s : Set ℂ} (hs : s.Countable) :
    IsPathConnected (Metric.ball z r \ s)