Hopf problem: foundations · complex

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SchwarzReflection.differentiableOn_of_continuousOn_off_real {U : Set ℂ} (hU : IsOpen U) {f : ℂ → ℂ} (hf : ContinuousOn f U) (hd : ∀ z ∈ U, z.im ≠ 0 → DifferentiableAt ℂ f z) : DifferentiableOn ℂ f U