English
For any x and subset C, ClusterPt x (𝓟 C) holds iff x ∈ C or AccPt x (𝓟 C).
Русский
Для любой x и подмножества C выполняется: ClusterPt x (𝓟 C) тогда и только тогда, когда x ∈ C или AccPt x (𝓟 C).
LaTeX
$$$ClusterPt\ x\ (\mathcal{P} C) \iff x \in C \lor AccPt\ x\ (\mathcal{P} C)$$$
Lean4
theorem clusterPt_principal {x : X} {C : Set X} : ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C) :=
by
constructor
· intro h
by_contra! hc
rw [accPt_principal_iff_clusterPt] at hc
simp_all only [not_false_eq_true, diff_singleton_eq_self, not_true_eq_false, hc.1]
· rintro (h | h)
· exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩
· exact h.clusterPt
