Hopf problem: period family · core 4 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.PeriodFamily.Homology.openPartitionInclusion_ne_mo1973_25234
{X : Type}
[TopologicalSpace X]
(U : Fin 3 → TopologicalSpace.Opens X)
(hdisj : Pairwise fun (i j : Fin 3) => Disjoint ↑(U i) ↑(U j))
{i j : Fin 3}
(hij : i ≠ j)
(x : ↥(U i))
(y : ↥(U j))
: