Euclidean spheres

This files defines the n-sphere 𝕊 n and the n-disk 𝔻 as objects in TopCat. The parameter n is in ℤ so as to facilitate the definition of CW-complexes (see the file Topology.CWComplex).

noncomputable def TopCat.sphere (n : ℤ) : TopCat

The n-sphere is the set of points in ℝⁿ⁺¹ whose norm equals 1, endowed with the subspace topology.

Equations

• TopCat.sphere n = TopCat.of (ULift.{?u.16, 0} ↑(Metric.sphere 0 1))

noncomputable def TopCat.disk (n : ℤ) : TopCat

The n-disk is the set of points in ℝⁿ whose norm is at most 1, endowed with the subspace topology.

Equations

• TopCat.disk n = TopCat.of (ULift.{?u.16, 0} ↑(Metric.closedBall 0 1))

def TopCat.term𝕊_ : Lean.ParserDescr

𝕊 n denotes the n-sphere.

Equations

• TopCat.term𝕊_ = Lean.ParserDescr.node `TopCat.term𝕊_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝕊 ") (Lean.ParserDescr.cat `term 1023))

def TopCat.term𝔻_ : Lean.ParserDescr

𝔻 n denotes the n-disk.

Equations

• TopCat.term𝔻_ = Lean.ParserDescr.node `TopCat.term𝔻_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝔻 ") (Lean.ParserDescr.cat `term 1023))