instAlexandrovDiscrete — Mathlib

English

The dependent sum Σ i, X_i is Alexandrov-discrete if every fiber X_i is Alexandrov-discrete and all necessary topological structures are in place.

Русский

Зависимая сумма Σ i, X_i Александрово-дискретна, если все слои X_i Александрово-дискретны и заданы соответствующие топологии.

LaTeX

$$AlexandrovDiscrete ((i, X_i))$$

Lean4

instance instAlexandrovDiscrete {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, AlexandrovDiscrete (X i)] : AlexandrovDiscrete (Σ i, X i) :=
  alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced

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