deltaGeneratedSpace_deltaGenerated

English

The delta-generated topology on X turns X into a delta-generated space.

Русский

Дельта-генерируемая топология на X делает из X дельта-генерируемое пространство.

LaTeX

$$$$\DeltaGeneratedSpace(X, \deltaGenerated X)$$$$

Lean4

/-- The delta-generated topology on `X` does in fact turn `X` into a delta-generated space. -/
theorem deltaGeneratedSpace_deltaGenerated {X : Type*} {t : TopologicalSpace X} :
    @DeltaGeneratedSpace X (@deltaGenerated X t) := by let _ := @deltaGenerated X t; constructor;
  rw [@deltaGenerated_deltaGenerated_eq X t]

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