nhdsSet_prod_eq_biSup — Mathlib

English

If K is compact and for every x ∈ K we have s ∈ 𝓝 x ×ˢ l, then s ∈ (nhdsSet K) ×ˢ l.

Русский

Если K компактно и для каждого x ∈ K выполняется s ∈ 𝓝 x ×ˢ l, то s ∈ (nhdsSet K) ×ˢ l.

LaTeX

$$$IsCompact\\,K \\rightarrow (\\\\forall x \\in K, s \\in 𝓝 x \\timesˢ l) \\\\rightarrow s \\in (\\\\nhdsSet K) \\timesˢ l$$$

Lean4

theorem nhdsSet_prod_eq_biSup {K : Set X} (hK : IsCompact K) {Y} (l : Filter Y) : (𝓝ˢ K) ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l :=
  le_antisymm (fun s hs ↦ hK.mem_nhdsSet_prod_of_forall <| by simpa using hs)
    (iSup₂_le fun _ hx ↦ prod_mono (nhds_le_nhdsSet hx) le_rfl)

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