English
In a second-countable space, any open set that is a union of open sets is a countable union of some of them.
Русский
В пространстве с двойной счетностью любой открытый набор, представимый как объединение открытых множеств, равен объединению счётного подмножества этих множеств.
LaTeX
$$$[SecondCountableTopology\ \alpha] \; {t : Set(Set(\alpha))}\; (IsTopologicalBasis\ t) \Rightarrow \exists\ s \subseteq t, s.Countable \land \alpha\ = \bigcup_{a \in s} a$$$
Lean4
/-- In a second-countable space, an open set, given as a union of open sets,
is equal to the union of countably many of those sets.
In particular, any open covering of `α` has a countable subcover: α is a Lindelöf space. -/
theorem isOpen_iUnion_countable [SecondCountableTopology α] {ι} (s : ι → Set α) (H : ∀ i, IsOpen (s i)) :
∃ T : Set ι, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i :=
by
let B := {b ∈ countableBasis α | ∃ i, b ⊆ s i}
choose f hf using fun b : B => b.2.2
haveI : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype
refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩
rintro _ ⟨i, rfl⟩ x xs
rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩
