Hopf problem: pi 1 · threefold overlap mapping torus 1

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

@[reducible, inline]

abbrev Mathoverflow1973.ThreefoldOverlapMappingTorus.Radius (n : ℕ) (r : ℝ) : Type

Radii whose nth powers lie below a prescribed bound.

Equations

• Mathoverflow1973.ThreefoldOverlapMappingTorus.Radius n r = { a : ℝ // 0 < a ∧ a < 1 ∧ a ^ n < r }

theorem Mathoverflow1973.ThreefoldOverlapMappingTorus.radius_nonempty (n : ℕ) (hn : 0 < n) (r : ℝ) (hr : 0 < r) : Nonempty (Radius n r)