English
Let V_i be a directed family of compact, closed subsets of X, and U a set such that U is a neighborhood of every point in ⋂ V_i. Then there exists i with V_i ⊆ U.
Русский
Пусть V_i образуют направленную по включению семью компактных замкнутых подмножеств X, и U такая, что U является окрестностью каждой точки ⋂ V_i. Тогда существует i, такой что V_i ⊆ U.
LaTeX
$$$\text{Directed} (\,\supseteq\,)\nV \Rightarrow (\forall i, \operatorname{IsCompact}(V_i)) \land (\forall i, \operatorname{IsClosed}(V_i)) \Rightarrow \forall U,\left(\forall x \in \bigcap_i V_i, U \in \mathcal{N}_x\right) \Rightarrow \exists i\, V_i \subseteq U$$$
Lean4
/-- If `V : ι → Set X` is a decreasing family of closed compact sets then any neighborhood of
`⋂ i, V i` contains some `V i`. We assume each `V i` is compact *and* closed because `X` is
not assumed to be Hausdorff. See `exists_subset_nhds_of_compact` for version assuming this. -/
theorem exists_subset_nhds_of_isCompact' [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V)
(hV_cpct : ∀ i, IsCompact (V i)) (hV_closed : ∀ i, IsClosed (V i)) {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) :
∃ i, V i ⊆ U := by
obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
by_contra! H
replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
have : (⋂ i, V i ∩ Wᶜ).Nonempty :=
by
refine
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
(fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i => (hV_closed i).inter W_op.isClosed_compl
rcases hV i j with ⟨k, hki, hkj⟩
refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;> tauto
have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
contradiction
