English
If s and t are compact subsets of a Hausdorff space X, then the set-theoretic neighborhood filter of their intersection equals the infimum of the neighborhood filters of each set: nhdsSet(s ∩ t) = nhdsSet(s) ⊓ nhdsSet(t).
Русский
Пусть s и t — компактные подмножества Х, где Х — хаусдорфово. Тогда фильтр окрестностей множества s ∩ t равен инфимума фильтров окрестностей s и t: 𝒩ˢ(s∩t) = 𝒩ˢ s ⊓ 𝒩ˢ t.
LaTeX
$$$\forall X,[TopologicalSpace\ X],[T2Space\ X],\forall s,t\subseteq X\\,\text{ IsCompact } s\land IsCompact t\Rightarrow 𝓝ˢ(s\cap t)=𝓝ˢ s\;\sqcap\; 𝓝ˢ t$$$
Lean4
/-- If `s` and `t` are compact sets in a T₂ space, then the set neighborhoods filter of `s ∩ t`
is the infimum of set neighborhoods filters for `s` and `t`.
For general sets, only the `≤` inequality holds, see `nhdsSet_inter_le`. -/
theorem nhdsSet_inter_eq [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t :=
by
refine le_antisymm (nhdsSet_inter_le _ _) ?_
simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]
refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_
rcases eq_or_ne x y with (rfl | hne)
· exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le
· exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le
