clusterPt_principal_iff_frequently

English

Let s be a subset of X. Then x is a cluster point of the principal filter by s if and only if there exists a frequently occurring point y in the neighborhoods of x with y ∈ s.

Русский

Пусть s ⊆ X. Тогда x является кластерной точкой Principal(s) тогда и только тогда, когда существует часто встречающееся число y в окрестностях x такое, что y ∈ s.

LaTeX

$$$\\mathrm{ClusterPt}(x,\\mathcal{P}(s)) \\iff \\exists^{\\mathrm{freq}}\, y \\in \\mathcal{N}(x),\, y \\in s$$$

Lean4

theorem clusterPt_principal_iff_frequently : ClusterPt x (𝓟 s) ↔ ∃ᶠ y in 𝓝 x, y ∈ s := by
  simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, mem_inter_iff]

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