Jordan Curve Theorem/Brouwer Fixed Point Theorem

Stream: Is there code for X?

[Evan Bailey]

Have Brouwer's Fixed Point Theorem and/or the Jordan Curve Theorem (or any generalizations thereof) been added to Mathlib4 yet? I see here that at least Brouwer's Fixed Point Theorem has been formalized, but I cannot find it in Mathlib.

If not, is there an ongoing project to add them? If not, I would be interested adding them (especially since the Tietze extension theorem already exists), although there is a chance I am drastically understimating the amount of work this would take.

[Vincent Beffara]

There is a lean3 version of Brouwer there: https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/brouwer_fixed_point.lean (with an amusing blueprint within), which is linked to from 100.yaml indeed, but AFAIK we don't have the Jordan curve theorem.

[Vincent Beffara]

If I understand it right, it has been formalized in Isabelle : https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Jordan_Curve.html