Euclidean spheres

This files defines the n-sphere 𝕊 n, the n-disk 𝔻 n and its boundary ∂𝔻 n as objects in TopCat.

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.12, 0} ↑(Metric.closedBall 0 1))

noncomputable def TopCat.diskBoundary (n : ℕ) : TopCat

The boundary of the n-disk.

Equations

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

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.diskBoundary (n + 1)

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))

def TopCat.«term∂𝔻_» : Lean.ParserDescr

∂𝔻 n denotes the boundary of the n-disk.

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-sphere.

Equations

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

def TopCat.diskBoundaryInclusion (n : ℕ) : diskBoundary n ⟶ disk n

The inclusion ∂𝔻 n ⟶ 𝔻 n of the boundary of the n-disk.

Equations

• One or more equations did not get rendered due to their size.