English
The neighborhood at a from the intersection s ∩ t equals the infimum of the neighborhood filters within s and within t.
Русский
Окрестность в a от пересечения s ∩ t равна наименьшему (infimum) из 𝓝[s] a и 𝓝[t] a.
LaTeX
$$$$ 𝓝[s \\cap t](a) = 𝓝[s](a) \\wedge 𝓝[t](a) $$$$
Lean4
theorem nhdsWithin_inter (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a :=
by
delta nhdsWithin
rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]