English
For a Lindelöf s and a family of sets c_i with indexed by b, if c_i are open on b and s is covered by ∪_{i∈b} c_i, there exists b' ⊆ b such that s ⊆ ∪_{i∈b'} c_i.
Русский
Для Линдельёфово s и семейство c_i открыто на b, если s ⊆ ⋃_{i∈b} c_i, то существует b' ⊆ b такое, что s ⊆ ⋃_{i∈b'} c_i.
LaTeX
$$$IsLindelof(s) \to (c_i)_{i\in b} \text{ открыты} \land s \subseteq \bigcup_{i\in b} c_i \to \exists b'\subseteq b, b'\ countable \land s \subseteq \bigcup_{i\in b'} c_i.$$$
Lean4
/-- For every open cover of a Lindelöf set, there exists a countable subcover. -/
theorem elim_countable_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsLindelof s) (hc₁ : ∀ i ∈ b, IsOpen (c i))
(hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b', b' ⊆ b ∧ Set.Countable b' ∧ s ⊆ ⋃ i ∈ b', c i :=
by
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
rcases hs.elim_countable_subcover (fun i ↦ c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩
rw [biUnion_image]
exact hd.2
