English
For x ∈ X and s ⊆ X, the filter 𝓝[s] x is nontrivial iff every neighborhood t ∈ 𝓝(x) has a nonempty intersection with s.
Русский
Для x и s: 𝓝[s] x не тривиален тогда, когда для каждого окрестности t ∈ 𝓝(x) пересечение t ∩ s непусто.
LaTeX
$$$(𝓝[s] x).NeBot \\iff \\forall t \\in \\mathcal{N}(x), (t \\cap s) \\neq \\emptyset$$$
Lean4
theorem nhdsWithin_neBot : (𝓝[s] x).NeBot ↔ ∀ ⦃t⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty :=
by
rw [nhdsWithin, inf_neBot_iff]
exact
forall₂_congr fun U _ ↦ ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩