English
For a Lindelöf set s and a filter l with countable intersection, the neighborhood filter of s is disjoint from l if and only if for every x in s, the neighborhood filter at x is disjoint from l.
Русский
Для множества s Линдельёфово и фильтра l с CPIP, дисжойнт NHDS(s) и l эквивалентен тому, что для каждого x∈s дисжойнт NHDS(x) и l.
LaTeX
$$$Disjoint (\mathcal{N}_s)\, l \iff \forall x\in s,\ Disjoint (\mathcal{N}_x)\ l.$$$
Lean4
/-- The neighborhood filter of a Lindelöf set is disjoint with a filter `l` with the countable
intersection property if and only if the neighborhood filter of each point of this set
is disjoint with `l`. -/
theorem disjoint_nhdsSet_left {l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) :
Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l :=
by
refine ⟨fun h x hx ↦ h.mono_left <| nhds_le_nhdsSet hx, fun H ↦ ?_⟩
choose! U hxU hUl using fun x hx ↦ (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
choose hxU hUo using hxU
rcases hs.elim_nhds_subcover U fun x hx ↦ (hUo x hx).mem_nhds (hxU x hx) with ⟨t, htc, hts, hst⟩
refine (hasBasis_nhdsSet _).disjoint_iff_left.2 ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx ↦ hUo x (hts x hx), hst⟩, ?_⟩
rw [compl_iUnion₂]
exact (countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))
