English
If a directed family of compact sets has a common neighborhood property, then some member of the family is contained in a prescribed neighborhood.
Русский
Если направленная семействa компактных множеств обладает общей свойством окрестности, существует элемент семьи, включенный в заданную окрестность.
LaTeX
$$$\\exists i, V_i \\subset U$ под заданными условиями (набор формулировок через directed и IsCompact).$$$
Lean4
/-- If `V : ι → Set X` is a decreasing family of compact sets then any neighborhood of
`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
don't need to assume each `V i` closed because it follows from compactness since `X` is
assumed to be Hausdorff. -/
theorem exists_subset_nhds_of_isCompact [T2Space X] {ι : Type*} [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V)
(hV_cpct : ∀ i, IsCompact (V i)) {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U :=
exists_subset_nhds_of_isCompact' hV hV_cpct (fun i => (hV_cpct i).isClosed) hU
