nhdsSet_inf_eq_biSup — Mathlib

English

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

Русский

Для компактного K, инфимум nhdsSet K ∩ l равен наибольшему нижнему пределу по x∈K от nhds x ∩ l.

LaTeX

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

Lean4

theorem nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) : (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l :=
  by
  have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by
    simpa only [comap_prod] using congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm
  simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]

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