Theorem Complex.isConnected_of_lowerHalfPlane

Modification history

2025-09-12 12:47
Mathlib/Analysis/Complex/Convex.lean
feat: a complex differentiable function on a disk has a primitive (#9598) …
Modified Complex.isConnected_of_lowerHalfPlaneView on Github →
2024-11-10 20:16
Mathlib/Analysis/Complex/Convex.lean
refactor(Analysis/Complex): merge Complex/Convex and Convex/Complex (#18819) …
Modified Complex.isConnected_of_lowerHalfPlaneView on Github →
2024-08-16 23:11
Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
feat: better proof of spectral permanence (#15603) …
Added Complex.isConnected_of_lowerHalfPlaneView on Github →