Hopf problem: uniformization · special periods 1

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

def Mathoverflow1973.SpecialPeriods.unitDisc : TopologicalSpace.Opens ℂ

The open unit disc in the complex plane.

Equations

• Mathoverflow1973.SpecialPeriods.unitDisc = { carrier := Metric.ball 0 1, is_open' := Mathoverflow1973.SpecialPeriods.unitDisc._proof_1✝ }

@[reducible, inline]

abbrev Mathoverflow1973.SpecialPeriods.Disc : TopologicalSpace.Opens ℂ

The complex open unit disc as a subtype.

Equations

• Mathoverflow1973.SpecialPeriods.Disc = Mathoverflow1973.SpecialPeriods.unitDisc