accPt_principal_iff_clusterPt — Mathlib

English

For any x and C ⊆ X, AccPt x (𝓟 C) iff ClusterPt x (𝓟 (C \\ {x})).

Русский

Для любой x и C ⊆ X, AccPt x (Principal C) эквивалентно ClusterPt x (Principal (C \\ {x})).

LaTeX

$$$\\mathrm{AccPt}(x, \\mathcal{P}(C)) \\iff \\mathrm{ClusterPt}(x, \\mathcal{P}(C \\ {x}))$$$

Lean4

/-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`. -/
theorem accPt_principal_iff_clusterPt {x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ { x })) := by
  rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]

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