English
Let S ⊆ X and x ∈ S. The nontrivial nhds on S at x is nontrivial iff the nontrivial nhds on X at x, intersected with 𝓟S, is nontrivial.
Русский
Пусть S ⊆ X и x ∈ S. Непустой фильтр окрестностей на подмножестве S в точке x эквивалентен непустому фильтру окрестностей в X, пересечённому с 𝓟S.
LaTeX
$$$$ (\\mathcal N^{\\neq}_S(x)).NeBot \\iff (\\mathcal N^{\\neq}_X(x) \\sqcap \\mathcal P(S)).NeBot $$$$
Lean4
theorem nhds_ne_subtype_neBot_iff {S : Set X} {x : S} : (𝓝[≠] x).NeBot ↔ (𝓝[≠] (x : X) ⊓ 𝓟 S).NeBot := by
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]