prod_nhdsSet_eq_biSup — Mathlib

English

For a compact K, the product l ×ˢ 𝓝ˢ K equals the supremum over x ∈ K of l ×ˢ 𝓝 x.

Русский

Для компактного K произведение l ×ˢ 𝓝ˢ K равно верхней границе по x∈K множества l ×ˢ 𝓝 x.

LaTeX

$$$ l \\timesˢ 𝓝ˢ K = \\bigvee_{x \\in K} l \\timesˢ 𝓝 x $$$

Lean4

theorem prod_nhdsSet_eq_biSup {K : Set Y} (hK : IsCompact K) {X} (l : Filter X) : l ×ˢ (𝓝ˢ K) = ⨆ y ∈ K, l ×ˢ 𝓝 y := by
  simp only [prod_comm (f := l), hK.nhdsSet_prod_eq_biSup, map_iSup]

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