Delta-generated topological spaces

This file defines delta-generated spaces, as topological spaces whose topology is coinduced by all maps from Euclidean spaces into them. This is the strongest topological property that holds for all CW-complexes and is closed under quotients and disjoint unions; every delta-generated space is locally path-connected, sequential and in particular compactly generated.

See https://ncatlab.org/nlab/show/Delta-generated+topological+space.

The notions defined in this file (see also the file Mathlib/Topology/Category/DeltaGenerated.lean for the category DeltaGenerated) are a particular case of the notion of X-generated topological spaces where X is a family of topological spaces (see the file Mathlib/Topology/Convenient/GeneratedBy.lean.)

TODO

• All locally path-connected first-countable spaces are delta-generated - in particular, all normed spaces and convex subsets thereof, like the standard simplices and the unit interval.
• Delta-generated spaces are equivalently generated by the simplices Δⁿ.
• Delta-generated spaces are equivalently generated by the unit interval I.

@[reducible, inline]

abbrev DeltaGeneratedSpace (Y : Type u_1) [TopologicalSpace Y] : Prop

A topological space is Delta-generated if its topology is generated by the continuous maps from topological spaces of the form Fin n → ℝ.

Equations

• DeltaGeneratedSpace Y = Topology.IsGeneratedBy (fun (n : ℕ) => Fin n → ℝ) Y

@[reducible, inline]

abbrev DeltaGeneratedSpace.of {Y : Type u_2} [TopologicalSpace Y] : Type u_2

Type synonym to be equipped with the delta-generated topology.

Equations

• DeltaGeneratedSpace.of = Topology.WithGeneratedByTopology (fun (n : ℕ) => Fin n → ℝ) Y

instance DeltaGeneratedSpace.instLocallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [DeltaGeneratedSpace X] : LocallyPathConnectedSpace X

Delta-generated spaces are locally path-connected.

instance DeltaGeneratedSpace.instSequentialSpace {X : Type u_1} [TopologicalSpace X] [DeltaGeneratedSpace X] : SequentialSpace X

Delta-generated spaces are sequential.