inf_nhdsSet_eq_biSup — Mathlib

English

For a compact K, the infimum of l and nhdsSet K equals the supremum over x ∈ K of nhds x inf l.

Русский

Для компактного K инфимум l и nhdsSet K равен супремуму по x∈K от nhds x ∩ l.

LaTeX

$$$l \\cap nhdsSet K = \\bigvee_{x \\in K} (nhds x \\cap l)$$$

Lean4

theorem inf_nhdsSet_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) : l ⊓ (𝓝ˢ K) = ⨆ x ∈ K, l ⊓ 𝓝 x := by
  simp only [inf_comm l, hK.nhdsSet_inf_eq_biSup]

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