Commit 2024-01-31 14:30 1a65f05e

View on Github →

feat: characterize ClusterPt, MapClusterPt, IsClosed using ultrafilters (#10143) Preliminaries for #6844

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem clusterPt_iff_ultrafilter

added theorem isClosed_iff_ultrafilter

added theorem mapClusterPt_def

added theorem mapClusterPt_iff_ultrafilter