Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 20:38 352e0642

View on Github →

feat(topology/uniform_space/cauchy): add a few lemmas (#11912)

Estimated changes

Modified src/topology/uniform_space/cauchy.lean

added theorem cauchy.ultrafilter_of

added theorem complete_space_iff_ultrafilter

deleted theorem is_compact.is_complete

added theorem is_complete_iff_cluster_pt

added theorem is_complete_iff_ultrafilter'

added theorem is_complete_iff_ultrafilter