Documentation

TauCeti.Topology.Homeomorph.FixedPoint

The fixed-point property is invariant under homeomorphisms #

A topological space has the fixed-point property when every continuous self-map has a fixed point. Conjugating a self-map by a homeomorphism h : X ≃ₜ Y matches the fixed points of the two maps, so X has the fixed-point property exactly when Y does (Homeomorph.forall_exists_isFixedPt_iff). This transports Brouwer's fixed-point theorem from the disk to every space homeomorphic to it.

theorem Homeomorph.forall_exists_isFixedPt_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
(∀ (f : C(X, X)), ∃ (x : X), Function.IsFixedPt (⇑f) x) ↔ ∀ (g : C(Y, Y)), ∃ (y : Y), Function.IsFixedPt (⇑g) y

Homeomorphic spaces have the fixed-point property together: every continuous self-map of X has a fixed point exactly when every continuous self-map of Y does.