clusterPt_iff_frequently' — Mathlib

English

ClusterPt x F is equivalent to not being disjoint from nhds x and F.

Русский

Кластерная точка x относительно F эквивалентна тому, что множество nhds x и F не перестыкуются.

LaTeX

$$$\operatorname{ClusterPt} x F \iff \neg \operatorname{Disjoint}(\mathcal{N}(x), F)$$$

Lean4

theorem clusterPt_iff_frequently' {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : F.HasBasis p s) :
    ClusterPt x F ↔ ∀ i, p i → ∃ᶠ x in 𝓝 x, x ∈ s i :=
  by
  simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]
  exact ⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩

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