mem_nhdsSet_inf_of_forall — Mathlib

English

If K is compact and for all x ∈ K, s ∈ nhds x ∩ l, then s ∈ nhdsSet K ∩ l.

Русский

Если K компактно и для всех x ∈ K выполняется s ∈ nhds x ∩ l, то s ∈ nhdsSet K ∩ l.

LaTeX

$$$IsCompact\\,K \\rightarrow (\\\\forall x \\in K, s \\in nhds x \\cap l) \\rightarrow s \\in nhdsSet K \\cap l$$$

Lean4

/-- If `s : Set X` belongs to `𝓝 x ⊓ l` for all `x` from a compact set `K`,
then it belongs to `(𝓝ˢ K) ⊓ l`,
i.e., there exist an open `U ⊇ K` and `T ∈ l` such that `U ∩ T ⊆ s`. -/
theorem mem_nhdsSet_inf_of_forall {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K)
    (hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l) : s ∈ (𝓝ˢ K) ⊓ l :=
  (hK.nhdsSet_inf_eq_biSup l).symm ▸ by simpa using hs

Похожие утверждения