Hopf problem: cusp fibre · cusp central homology 3

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

theorem Mathoverflow1973.CuspCentralHomology.coverHomology_subsingleton_of_vanishing {X : Type} [TopologicalSpace X] (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hcover : U ∪ V = Set.univ) (n : ℕ) [Subsingleton ↑(SingularMayerVietoris.SingularHomology (↑U) (n + 1))] [Subsingleton ↑(SingularMayerVietoris.SingularHomology (↑V) (n + 1))] [Subsingleton ↑(SingularMayerVietoris.SingularHomology (↑(U ∩ V)) n)] : Subsingleton ↑(SingularMayerVietoris.SingularHomology X (n + 1))