Does Lean 4 currently have Brouwer’s fixed-point theorem?

Stream: lean4

[东禹]

Does Lean 4 currently have Brouwer’s fixed-point theorem?TT

[Kenny Lau]

https://leansearch.net/?q=Brouwer’s+fixed-point+theorem

[Aaron Liu]

I also have a proof of Brouwer's Fixed Point Theorem for a 2d disk (700 lines and ugly) if you need that

[东禹]

hahaThank you，let me see if I can skip this theorem.