English
A sum type of two second-countable spaces is second-countable.
Русский
Сумма двух пространств со второй счетностью также имеет вторую счетность.
LaTeX
$$$[SecondCountableTopology(\alpha)] \land [SecondCountableTopology(\beta)] \Rightarrow SecondCountableTopology(\alpha \oplus \beta)$$$
Lean4
/-- A sum type of two second countable spaces is second countable. -/
instance [SecondCountableTopology α] [SecondCountableTopology β] : SecondCountableTopology (α ⊕ β) :=
by
let b := (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
have B : b.Countable :=
(Countable.image (countable_countableBasis _) _).union (Countable.image (countable_countableBasis _) _)
exact A.secondCountableTopology B
