English
The neighborhood filter of a compact set is disjoint with a filter l iff the neighborhood filter at every point x ∈ s is disjoint with l.
Русский
Непрерывная окрестностная фильтрация компактного множества дисjoint с фильтром l тогда и только тогда, когда для каждой точки x ∈ s окрестностная фильтрация nhds x дисjoint с l.
LaTeX
$$$IsCompact(s) \rightarrow Disjoint (𝓝ˢ s) l \leftrightarrow \forall x \in s, Disjoint (𝓝 x) l$$$
Lean4
/-- The neighborhood filter of a compact set is disjoint with a filter `l` if and only if the
neighborhood filter of each point of this set is disjoint with `l`. -/
theorem disjoint_nhdsSet_left {l : Filter X} (hs : IsCompact 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, 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₂, biInter_finset_mem]
exact fun x hx => hUl x (hts x hx)
