mem_prod_nhdsSet_of_forall — Mathlib

English

If K is compact and for all y ∈ K, s ∈ nhds y ×ˢ l, then s ∈ nhdsSet K ×ˢ l.

Русский

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

LaTeX

$$$IsCompact\\,K \\rightarrow (\\\\forall y \\in K, s \\in nhds y \\timesˢ l) \\rightarrow s \\in nhdsSet K \\timesˢ l$$$

Lean4

/-- If `s : Set (X × Y)` belongs to `l ×ˢ 𝓝 y` for all `y` 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_prod_nhdsSet_of_forall {K : Set Y} {X} {l : Filter X} {s : Set (X × Y)} (hK : IsCompact K)
    (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K :=
  (hK.prod_nhdsSet_eq_biSup l).symm ▸ by simpa using hs

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