Hopf problem: threefold · special periods 6

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

def Mathoverflow1973.SpecialPeriods.Threefold.coordinateBall (r : ℝ) : TopologicalSpace.Opens ℂ

The open complex coordinate ball of radius r.

Equations

• Mathoverflow1973.SpecialPeriods.Threefold.coordinateBall r = { carrier := Metric.ball 0 r, is_open' := ⋯ }

@[simp]

theorem Mathoverflow1973.SpecialPeriods.Threefold.mem_coordinateBall (r : ℝ) (z : ℂ) : z ∈ coordinateBall r ↔ z ∈ Metric.ball 0 r