English
Let s ⊆ X and t ⊆ Y be compact. Then the set-neighborhood filter of s × t in X × Y equals the product of the set-neighborhood filters of s and t: 𝓝ˢ(s × t) = 𝓝ˢ s × 𝓝ˢ t.
Русский
Пусть s ⊆ X и t ⊆ Y — компактные множества. Тогда фильтр окрестностей множества s × t в X × Y равен произведению фильтров окрестностей s и t: 𝓝ˢ(s × t) = 𝓝ˢ s × 𝓝ˢ t.
LaTeX
$$$\mathcal{N}_{\mathrm{set}}(s \times t) = \mathcal{N}_{\mathrm{set}}(s) \times \mathcal{N}_{\mathrm{set}}(t)$$$
Lean4
/-- If `s` and `t` are compact sets, then the set neighborhoods filter of `s ×ˢ t`
is the product of set neighborhoods filters for `s` and `t`.
For general sets, only the `≤` inequality holds, see `nhdsSet_prod_le`. -/
theorem nhdsSet_prod_eq {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t := by
simp_rw [hs.nhdsSet_prod_eq_biSup, ht.prod_nhdsSet_eq_biSup, nhdsSet, sSup_image, biSup_prod, nhds_prod_eq]
