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.

@[implicit_reducible, deprecated "Use TopologicalSpace.generatedBy" (since := "2026-04-23")]

def TopologicalSpace.deltaGenerated (X : Type u_1) [TopologicalSpace X] : TopologicalSpace X

The topology coinduced by all maps from ℝⁿ into a space.

Equations

• TopologicalSpace.deltaGenerated X = ⨆ (f : (n : ℕ) × C(Fin n → ℝ, X)), TopologicalSpace.coinduced (⇑f.snd) inferInstance

@[deprecated TopologicalSpace.generatedBy_eq_coinduced (since := "2026-04-23")]

theorem deltaGenerated_eq_coinduced {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : TopologicalSpace.generatedBy X = TopologicalSpace.coinduced (fun (x : (f : (i : ι) × C(X i, Y)) × X f.fst) => x.fst.snd x.snd) inferInstance

Alias of TopologicalSpace.generatedBy_eq_coinduced.

@[deprecated TopologicalSpace.generatedBy_le (since := "2026-04-23")]

theorem deltaGenerated_le {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} : TopologicalSpace.generatedBy X ≤ tY

Alias of TopologicalSpace.generatedBy_le.

@[deprecated Topology.WithGeneratedByTopology.isOpen_iff (since := "2026-04-23")]

theorem isOpen_deltaGenerated_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {U : Set (Topology.WithGeneratedByTopology X Y)} : IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' ⇑Topology.WithGeneratedByTopology.equiv.symm ⁻¹' U)

Alias of Topology.WithGeneratedByTopology.isOpen_iff.

@[deprecated TopologicalSpace.generatedBy_generatedBy (since := "2026-04-23")]

theorem deltaGenerated_deltaGenerated_eq {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : Type u_1) [TopologicalSpace Y] : TopologicalSpace.generatedBy X = TopologicalSpace.generatedBy X

Alias of TopologicalSpace.generatedBy_generatedBy.

@[deprecated Topology.IsGeneratedBy.generatedBy_eq (since := "2026-04-23")]

theorem eq_deltaGenerated {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} [Topology.IsGeneratedBy X Y] : TopologicalSpace.generatedBy X = tY

Alias of Topology.IsGeneratedBy.generatedBy_eq.

@[deprecated Topology.IsGeneratedBy.isOpen_iff (since := "2026-04-23")]

theorem DeltaGeneratedSpace.isOpen_iff {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [Topology.IsGeneratedBy X Y] {U : Set Y} : IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' U)

Alias of Topology.IsGeneratedBy.isOpen_iff.

@[deprecated Topology.IsGeneratedBy.continuous_iff (since := "2026-04-23")]

theorem DeltaGeneratedSpace.continuous_iff {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] [Topology.IsGeneratedBy X Y] (g : Y → Z) : Continuous g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)

Alias of Topology.IsGeneratedBy.continuous_iff.

@[deprecated Topology.WithGeneratedByTopology.continuous_equiv (since := "2026-04-23")]

theorem continuous_to_deltaGenerated {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : Continuous ⇑Topology.WithGeneratedByTopology.equiv

Alias of Topology.WithGeneratedByTopology.continuous_equiv.

@[deprecated Topology.IsGeneratedBy.instWithGeneratedByTopology (since := "2026-04-23")]

theorem deltaGeneratedSpace_deltaGenerated {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : Topology.IsGeneratedBy X (Topology.WithGeneratedByTopology X Y)

Alias of Topology.IsGeneratedBy.instWithGeneratedByTopology.

@[deprecated TopologicalSpace.generatedBy_mono (since := "2026-04-23")]

theorem deltaGenerated_mono {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {t₁ t₂ : TopologicalSpace Y} (h : t₁ ≤ t₂) : TopologicalSpace.generatedBy X ≤ TopologicalSpace.generatedBy X

Alias of TopologicalSpace.generatedBy_mono.

@[deprecated Topology.WithGeneratedByTopology.equiv (since := "2026-04-23")]

def DeltaGeneratedSpace.counit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : Topology.WithGeneratedByTopology X Y ≃ Y

Alias of Topology.WithGeneratedByTopology.equiv.

Equations

• @DeltaGeneratedSpace.counit = @Topology.WithGeneratedByTopology.equiv

@[deprecated Topology.WithGeneratedByTopology.continuous_equiv (since := "2026-04-23")]

theorem DeltaGeneratedSpace.continuous_counit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : Continuous ⇑Topology.WithGeneratedByTopology.equiv

Alias of Topology.WithGeneratedByTopology.continuous_equiv.

@[deprecated Topology.IsGeneratedBy.coinduced (since := "2026-04-23")]

theorem DeltaGeneratedSpace.coinduced {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [Topology.IsGeneratedBy X Y] (f : Y → Z) : Topology.IsGeneratedBy X Z

Alias of Topology.IsGeneratedBy.coinduced.

@[deprecated Topology.IsGeneratedBy.iSup (since := "2026-04-23")]

theorem DeltaGeneratedSpace.iSup {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {κ : Sort u_2} {t : κ → TopologicalSpace Y} (h : ∀ (k : κ), Topology.IsGeneratedBy X Y) : Topology.IsGeneratedBy X Y

Alias of Topology.IsGeneratedBy.iSup.

@[deprecated Topology.IsGeneratedBy.sup (since := "2026-04-23")]

theorem DeltaGeneratedSpace.sup {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {t₁ t₂ : TopologicalSpace Y} (h₁ : Topology.IsGeneratedBy X Y) (h₂ : Topology.IsGeneratedBy X Y) : Topology.IsGeneratedBy X Y

Alias of Topology.IsGeneratedBy.sup.

@[deprecated Topology.IsQuotientMap.isGeneratedBy (since := "2026-04-23")]

theorem Topology.IsQuotientMap.deltaGeneratedSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {f : Y → Z} (hf : IsQuotientMap f) [IsGeneratedBy X Y] : IsGeneratedBy X Z

Alias of Topology.IsQuotientMap.isGeneratedBy.

@[deprecated Quot.isGeneratedBy (since := "2026-04-23")]

theorem Quot.deltaGeneratedSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [Topology.IsGeneratedBy X Y] {r : Y → Y → Prop} : Topology.IsGeneratedBy X (Quot r)

Alias of Quot.isGeneratedBy.

@[deprecated Quotient.isGeneratedBy (since := "2026-04-23")]

theorem Quotient.deltaGeneratedSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [Topology.IsGeneratedBy X Y] {s : Setoid Y} : Topology.IsGeneratedBy X (Quotient s)

Alias of Quotient.isGeneratedBy.

@[deprecated Sum.isGeneratedBy (since := "2026-04-23")]

theorem Sum.deltaGeneratedSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] [Topology.IsGeneratedBy X Y] [Topology.IsGeneratedBy X Z] : Topology.IsGeneratedBy X (Y ⊕ Z)

Alias of Sum.isGeneratedBy.

@[deprecated Sigma.isGeneratedBy (since := "2026-04-23")]

theorem Sigma.deltaGeneratedSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {κ : Type u_1} {Y : κ → Type u_2} [(k : κ) → TopologicalSpace (Y k)] [∀ (k : κ), Topology.IsGeneratedBy X (Y k)] : Topology.IsGeneratedBy X ((k : κ) × Y k)

Alias of Sigma.isGeneratedBy.