English
If I is a set of indices and s(i) are open sets with I, then there exists a countable subcollection whose union equals the union over all I.
Русский
Если имеется множество индексов I и для каждого i∈I открытое множество s(i), то существует счётное подмножество, чья унион равна униону по всем I.
LaTeX
$$$[SecondCountableTopology\ α] (I : Set\, ι) (s : ι → Set α) (H : \forall i\in I, IsOpen(s(i))) : \exists T \subseteq I, T.Countable ∧ ⋃ i∈T, s(i) = ⋃ i∈I, s(i)$$$
Lean4
theorem isOpen_biUnion_countable [SecondCountableTopology α] {ι : Type*} (I : Set ι) (s : ι → Set α)
(H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i :=
by
simp_rw [← Subtype.exists_set_subtype, biUnion_image]
rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩
exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩
