instLindelofSpaceSigmaOfCountable

English

If each X_i is Lindelöf and the index set is countable, then the dependent sum Σ i, X_i is Lindelöf.

Русский

Если каждая X_i Линдельфова и индексный множество счётно, то зависимая сумма Σ_i X_i Линдельфова.

LaTeX

$$$[\\text{Countable }\\iota] \\forall i, \\operatorname{LindelofSpace}(X_i) \\Rightarrow \\operatorname{LindelofSpace}\\left(\\sum_{i} X_i\\right).$$$

Lean4

instance {X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)] [∀ i, LindelofSpace (X i)] :
    LindelofSpace (Σ i, X i) where
  isLindelof_univ := by
    rw [Sigma.univ]
    exact isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk

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