Jordan Curve Theorem (JCT) #35222
Description
Zulip:
- #maths > Multivariate complex analysis
- #mathlib4 > Jordan curve / Smooth Jordan curve
- #PR reviews > Polygons PR
- #new members > Board Games in Lean @ 💬
- #mathlib4 > What will the Jordan Curve Theorem look like in mathlib?
There is a proof using HOL-Light (the main theorem is let JORDAN_CURVE_THEOREM), essentially proven by a limiting argument of the polygonal case, but we plan to use machinery from algebraic topology to prove the n-dimensional case in general spaces.