topology.(at_point, principal_filter) are the same

[t6s]

Do we need to keep both?

Lemma at_pointE T (t : T) : at_point t = principal_filter t.
Proof.
by apply:funext=> S; apply: propext; split=> [? ? -> | /(_ t erefl)].
Qed.