Concatenation of winding numbers for absolutely continuous curves

For an absolutely continuous curve avoiding a point z on two intervals sharing an endpoint, the winding number over the combined interval is the sum of the winding numbers on the two pieces, in either orientation.

theorem AbsolutelyContinuousOnInterval.windingNumber_concat {γ : ℝ → ℂ} {a b c : ℝ} {z : ℂ} (h_ab : AbsolutelyContinuousOnInterval γ a b) (h_bc : AbsolutelyContinuousOnInterval γ b c) (hz_ab : z ∉ γ '' Set.uIcc a b) (hz_bc : z ∉ γ '' Set.uIcc b c) : TauCeti.Contour.windingNumber γ a c z = TauCeti.Contour.windingNumber γ a b z + TauCeti.Contour.windingNumber γ b c z

Off-trace additivity of the winding number over adjacent parameter intervals for an absolutely continuous curve, in either orientation.