English
If s is Lindelöf and t_i are closed such that ∀u countable, s ∩ ⋂_{i∈u} t_i is nonempty, then the full intersection s ∩ ⋂_{i} t_i is nonempty.
Русский
Если s — Линдельёфово, и t_i замкнуты так, что для каждого счётного подсемейства ⋂{i∈u} t_i пересекается с s, то ⋂_{i} t_i пересекается с s.
LaTeX
$$$IsLindelof(s) \to \forall t_i (IsClosed(t_i)) \to (\forall u \text{ countable}, (s \cap \bigcap_{i\in u} t_i).Nonempty) \Rightarrow (s \cap \bigcap_i t_i).Nonempty.$$$
Lean4
/-- A set `s` is Lindelöf if for every family of closed sets whose intersection avoids `s`,
there exists a countable subfamily whose intersection avoids `s`. -/
theorem isLindelof_of_countable_subfamily_closed
(h :
∀ {ι : Type u} (t : ι → Set X),
(∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅) :
IsLindelof s :=
isLindelof_of_countable_subcover fun U hUo hsU ↦
by
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
rcases h (fun i ↦ (U i)ᶜ) (fun i ↦ (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
refine ⟨t, ?_⟩
rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
