nhdsWithin_neBot — Mathlib

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⟩

Похожие утверждения