Documentation

Atlas.ComplexVariables.code.BridgeSingleSingularityBase

Bridge single singularity base — task verification #

bridge_single_singularity_base is a proved theorem in Lecture14.lean (line 615), reduced from circleIntegral_eq_sum_of_singularities with Fin 1.

The underlying axiom for the multi-singularity bridge construction is circleIntegral_eq_sum_of_singularities_bridge (line 559), which requires the Jordan curve theorem / piecewise smooth contour integration not in Mathlib.