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.