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.

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.

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.diskBoundaryInclusion (n : ℕ) : diskBoundary n ⟶ disk n

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