Borsuk separation criterion in Lean without homotopy lifting: open equivalence classes

Goal: if a, b are in the same component of ℂ \ K (K compact), then z ↦ (z-a)/(z-b) has a continuous argument on K. Skip path-lifting and homotopy lifting. Define R a c := 'has a continuous argument on K'. It is reflexive (θ = 0), symmetric (inverse, -θ) and transitive (product of the two quotients, θ₁+θ₂). If ‖c - a‖ < dist(a, K), then (z-a)/(z-c) has positive real part on K, so θ = Complex.arg is continuous there (Complex.continuousAt_arg needs slitPlane). So the classes are open, and so are their complements. IsPreconnected.subset_or_subset on connectedComponentIn then finishes. Janiszewski follows: two arguments on K₁ and K₂ differ on the preconnected K₁ ∩ K₂ by a function with values in 2πℤ, hence by a constant (its image is an interval inside 2πℤ). Shift one argument and glue with ContinuousOn.union_of_isClosed.