Euclidean spheres

This file 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.

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

The boundary of the n-disk.

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

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

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.

def TopCat.term𝔻_ : Lean.ParserDescr

𝔻 n denotes the n-disk.

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

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

def TopCat.term𝕊_ : Lean.ParserDescr

𝕊 n denotes the n-sphere.

def TopCat.term𝔹_ : Lean.ParserDescr

𝔹 n denotes the n-ball, the interior of the n-disk.

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

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

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

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

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)