Brouwer's fixed-point theorem for the plane disk

This file derives Brouwer's fixed-point theorem for the closed unit disk in Plane from no_retraction_planeClosedUnitBall.

If a continuous self-map f of the disk had no fixed point, the ray starting at f x and passing through x would meet the unit sphere in a continuously varying point. The positive root of the resulting quadratic equation gives this intersection explicitly. On the unit sphere that root is 1, so the construction would be a retraction of the disk onto its boundary, contradicting no_retraction_planeClosedUnitBall.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.fixedPointRayScale (p x : Plane) : ℝ

The scale at which the ray from p through x meets the unit sphere. Its intended use is when p lies in the unit ball and p ≠ x.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.fixedPointRayScale p x = (-inner ℝ p (x - p) + √(inner ℝ p (x - p) ^ 2 + inner ℝ (x - p) (x - p) * (1 - inner ℝ p p))) / inner ℝ (x - p) (x - p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.brouwer_fixed_point_planeClosedUnitBall (f : ↑(Metric.closedBall 0 1) → ↑(Metric.closedBall 0 1)) (hf : Continuous f) : ∃ (x : ↑(Metric.closedBall 0 1)), f x = x

Brouwer's fixed-point theorem for the closed unit disk in the Euclidean plane.

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.instBrouwerFixedPointPlane : InvarianceOfDomain.BrouwerFixedPoint Plane