Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 05:35 6dddef28

View on Github →

feat(topology/metric_space): range of a cauchy seq is bounded (#10423)

Estimated changes

Modified src/order/filter/cofinite.lean

added theorem filter.has_basis_cofinite

Modified src/topology/metric_space/basic.lean

added theorem metric.bounded_range_of_cauchy_map_cofinite

added theorem metric.bounded_range_of_tendsto_cofinite

added theorem metric.bounded_range_of_tendsto_cofinite_uniformity

Modified src/topology/uniform_space/cauchy.lean

modified theorem filter.has_basis.cauchy_iff