Documentation

LeanPool.HopfProblem.CuspFibre.CuspBoundaryTopVanishing

Hopf problem: cusp fibre · cusp boundary top vanishing #

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.CuspBoundaryGammaZero.equivariant_zpow_mo1973_29887 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ X) (g : Y ≃ₜ Y) (e : C(X, Y)) (he : ∀ (x : X), e (f x) = g (e x)) (n : ℤ) (x : X) :
e ((f ^ n) x) = (g ^ n) (e x)