Euclidean spheres

This files defines the n-sphere 𝕊 n, the n-disk 𝔻 n, its boundary ∂𝔻 n and its interior 𝔹 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.2, 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)

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

The n-ball is the set of points in ℝⁿ whose norm is strictly less than 1, endowed with the subspace topology.

Equations

• TopCat.ball n = TopCat.of (ULift.{?u.12, 0} ↑(Metric.ball 0 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.term𝔹_ : Lean.ParserDescr

𝔹 n denotes the n-ball, the interior 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.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.

def TopCat.ballInclusion (n : ℕ) : ball n ⟶ disk n

The inclusion 𝔹 n ⟶ 𝔻 n of the interior of the n-disk.

Equations

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

instance TopCat.instMonoDiskBoundaryInclusion {n : ℕ} : CategoryTheory.Mono (diskBoundaryInclusion n)

instance TopCat.instMonoBallInclusion {n : ℕ} : CategoryTheory.Mono (ballInclusion n)

instance TopCat.instCompactSpaceCarrierDisk (n : ℕ) : CompactSpace ↑(disk n)

instance TopCat.instCompactSpaceCarrierDiskBoundary (n : ℕ) : CompactSpace ↑(diskBoundary n)