English
For a compact K, the product neighborhood (nhdsSet K) × l is the supremum of the products nhds x × l over x ∈ K.
Русский
Для компактного K произведение окрестностей (nhdsSet K) × l является верхней гранью (супремумом) множества (nhds x) × l по x ∈ K.
LaTeX
$$$ (\\\\mathcal{N}^{s} K) \\\\times l = \\\\bigvee_{x \\in K} (\\\\mathcal{N} x \\\\times l) $$$
Lean4
/-- If `s : Set (X × Y)` belongs to `𝓝 x ×ˢ l` for all `x` from a compact set `K`,
then it belongs to `(𝓝ˢ K) ×ˢ l`,
i.e., there exist an open `U ⊇ K` and `t ∈ l` such that `U ×ˢ t ⊆ s`. -/
theorem mem_nhdsSet_prod_of_forall {K : Set X} {Y} {l : Filter Y} {s : Set (X × Y)} (hK : IsCompact K)
(hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l) : s ∈ (𝓝ˢ K) ×ˢ l :=
by
refine hK.induction_on (by simp) (fun t t' ht hs ↦ ?_) (fun t t' ht ht' ↦ ?_) fun x hx ↦ ?_
· exact prod_mono (nhdsSet_mono ht) le_rfl hs
· simp [sup_prod, *]
· rcases ((nhds_basis_opens _).prod l.basis_sets).mem_iff.1 (hs x hx) with ⟨⟨u, v⟩, ⟨⟨hx, huo⟩, hv⟩, hs⟩
refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩
exact prod_mem_prod (huo.mem_nhdsSet.2 Subset.rfl) hv
