English
If s is Lindelöf and (t_i) is a family of closed sets with s ∩ ⋂ t_i = ∅, then there exists a countable subfamily u of indices such that s ∩ ⋂_{i∈u} t_i = ∅.
Русский
Пусть s — множество Линдельёфа и (t_i) — семейство замкнутых множеств с условием s ∩ ⋂ i t_i = ∅. Тогда существует счётное подмножество индексов u такое, что s ∩ ⋂_{i∈u} t_i = ∅.
LaTeX
$$$IsLindelof(s) \to \forall(t_i) (\forall i, IsClosed(t_i)) \to (s \cap \bigcap_i t_i) = \emptyset \\to \exists u \subseteq I, u.Countable \land (s \cap \bigcap_{i\in u} t_i) = \emptyset.$$$
Lean4
/-- For every family of closed sets whose intersection avoids a Lindelöf set,
there exists a countable subfamily whose intersection avoids this Lindelöf set. -/
theorem elim_countable_subfamily_closed {ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i))
(hst : (s ∩ ⋂ i, t i) = ∅) : ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅ :=
by
let U := tᶜ
have hUo : ∀ i, IsOpen (U i) := by simp only [U, Pi.compl_apply, isOpen_compl_iff]; exact htc
have hsU : s ⊆ ⋃ i, U i := by
simp only [U, Pi.compl_apply]
rw [← compl_iInter]
apply disjoint_compl_left_iff_subset.mp
simp only [compl_iInter, compl_iUnion, compl_compl]
apply Disjoint.symm
exact disjoint_iff_inter_eq_empty.mpr hst
rcases hs.elim_countable_subcover U hUo hsU with ⟨u, ⟨hucount, husub⟩⟩
use u, hucount
rw [← disjoint_compl_left_iff_subset] at husub
simp only [U, Pi.compl_apply, compl_iUnion, compl_compl] at husub
exact disjoint_iff_inter_eq_empty.mp (Disjoint.symm husub)
