mem_inf_nhdsSet_of_forall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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