Delta-generated closed balls

A topological space is delta-generated (Mathlib's DeltaGeneratedSpace) when its topology is coinduced by all continuous maps from the spaces Fin n → ℝ. This file shows that every closed ball of a delta-generated real normed space, such as Fin n → ℝ, is delta-generated (TauCeti.instDeltaGeneratedSpaceClosedBall). An empty ball is covered by TauCeti.instIsGeneratedByOfIsEmpty. For a nonnegative radius, the radial retraction TauCeti.centeredRadialRetraction is a continuous retraction of the space onto the ball. A retraction is a quotient map, and quotients of delta-generated spaces are delta-generated.

The closed unit balls of Fin n → ℝ are the domains of the characteristic maps of a classical CW complex, so this is the input for showing that CW complexes are delta-generated, in TauCeti.Topology.CWComplex.Classical.DeltaGenerated.

instance TauCeti.instDeltaGeneratedSpaceClosedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [DeltaGeneratedSpace E] (x : E) (r : ℝ) : DeltaGeneratedSpace ↑(Metric.closedBall x r)

A closed ball of a delta-generated real normed space is delta-generated. This holds for every closed ball, including an empty one.