Theorem Brouwer Fixed Point Theorem For A Simplex

✓ theorem proved

#

Lean declarations

theorem Brouwer EconCSLib @ cef01c7, EconCSLib.Math.FixedPoint.Brouwer
```
theorem Brouwer (hf : Continuous f): ∃ x , f x = x
```

Modules: EconCSLib.Math.FixedPoint.Brouwer

Brouwer Fixed Point Theorem For A Simplex

Every continuous map $$ f:\Delta\to\Delta $$ from a simplex to itself has a fixed point.

References

[MFoGT, Cor. 4.11.2] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Continuous self-map of a simplex has a fixed point.

Used by

Fixed Point Theorem For Retracts Of A Simplex

Also in