Hopf problem: main theorem · six sphere cube 1

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

noncomputable def Mathoverflow1973.SixSphereCube.collapse {K : Type u_1} (F : Set K) (a : K) : OnePoint ↑Fᶜ

The map collapsing a subset to the point at infinity of its complement.

Equations

• Mathoverflow1973.SixSphereCube.collapse F a = if h : a ∈ F then OnePoint.infty else ↑⟨a, h⟩

theorem Mathoverflow1973.SixSphereCube.collapse_eq_iff {K : Type u_1} (F : Set K) (a b : K) : collapse F a = collapse F b ↔ a = b ∨ a ∈ F ∧ b ∈ F