Cluster point of principal filter

Stream: Is there code for X?

[Nir Paz]

Do we have something like this

theorem clusterPt_principal {X : Type u} [TopologicalSpace X] {a : X} {S : Set X}
    (h : ClusterPt a (𝓟 S)) : a ∈ S ∨ AccPt a (𝓟 S)

?

[Daniel Weber]

This should be fairly immediate from docs#acc_principal_iff_cluster