Brouwer fixed-point theorem (disc)
Closed
Theorem & proof
·
brouwer_disc.lean
·
✓ verified
1
2
3
import Mathlib theorem brouwer_disc {n : ℕ} (f : Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 → Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1) (hf : Continuous f) : ∃ x, f x = x :=sorry
Rewards pledged
No rewards pledged yet.