Hopf problem: toric · cusp honeycomb hexagon #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.CuspHoneycombRadial.exists_homeomorph_extending_frontier
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{K : Set E}
(hconv : Convex ℝ K)
(hclosed : IsClosed K)
(hbounded : Bornology.IsBounded K)
(hne : (interior K).Nonempty)
(e : ↑(frontier K) ≃ₜ ↑(frontier K))
: