instSecondCountableTopologySigmaOfCountable

English

In a disjoint union space Σ i, E_i, a topological basis is formed by taking the union of the bases on each component.

Русский

В дизъюнктном произведении Σ i, E_i базис получается как объединение базисов по каждой части пространства.

LaTeX

$$$IsTopologicalBasis(⋃ i, (fun u => (Sigma.mk i '' u)) '' s_i)$, где каждый $s_i$ является базисом на $E_i$$$

Lean4

/-- A countable disjoint union of second countable spaces is second countable. -/
instance [Countable ι] [∀ i, SecondCountableTopology (E i)] : SecondCountableTopology (Σ i, E i) :=
  by
  let b := ⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' countableBasis (E i)
  have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
  have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
  exact A.secondCountableTopology B

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