6.9. MappingDegree.ChartOverlapAvoidanceFull🔗

Jacobians.MappingDegree.ChartOverlapAvoidanceFull — source

exists_avoidance_in_open_chartedSpace_complex

Full chart-overlap avoidance for a ChartedSpace ℂ Y.

If Y is a charted space modelled on ℂ, U is open with y ∈ U, and C : Set Y is finite (no assumption that y ∉ C), there exists z ∈ U with z ∉ C and a path from y to z lying entirely in U.

Construction: take a ball-chart φ' at y (ChartRestrictionToBall), shrink its source to land inside U, then perturb (chartAt ℂ y) y along a straight segment in the chart ball whose pulled-back endpoint avoids C. Such a segment exists because the finite chart-image of C blocks at most finitely many directions through the centre.

theorem exists_avoidance_in_open_chartedSpace_complex
    {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {U : Set Y} (hU : IsOpen U) {y : Y} (hy : y ∈ U)
    {C : Set Y} (hC : C.Finite) :
    ∃ z : Y, z ∈ U ∧ z ∉ C ∧ JoinedIn U y z