deltaGeneratedSpace — Mathlib

English

The Sigma type consisting of delta-generated spaces is delta-generated.

Русский

Тип Σ, состоящий из дельта-генерируемых пространств, является дельта-генерируемым.

LaTeX

$$$$\DeltaGeneratedSpace(\Sigma i, X_i)$$$$

Lean4

/-- Disjoint unions of delta-generated spaces are delta-generated. -/
instance deltaGeneratedSpace {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, DeltaGeneratedSpace (X i)] : DeltaGeneratedSpace (Σ i, X i) :=
  .iSup fun _ ↦ .coinduced _

Похожие утверждения