Brouwer's fixed point theorem

Stream: Is there code for X?

[Jeremy Tan]

@Joël Riou is now porting a series of files in algebraic topology and the category-theoretic background behind them (just reached Moore complexes).

I just read about how algebraic topology can prove the Brouwer fixed point theorem; is there any proof of this in mathlib3?

[Jeremy Tan]

(And what about the other ones like Banach's?)

[Joël Riou]

It is not in mathlib, but you may look at this thread https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Completed.20proof.20of.20the.20Brouwer.20Fixed.20Point.20Theorem by @Brendan Seamas Murphy

[Yaël Dillies]

There's also an approach from Sperner's lemma, which shouldn't be too bad to finish from what we have. I've just had zero time for it.