Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-19 12:28 5ccf2bf2

View on Github →

feat(topology/metric_space/basic): an order-bounded set is metric-bounded (#8335)

Estimated changes

Modified src/topology/continuous_function/bounded.lean

Modified src/topology/metric_space/basic.lean

added theorem is_compact.bounded

added theorem metric.bounded_Icc

added theorem metric.bounded_Ico

added theorem metric.bounded_Ioc

added theorem metric.bounded_Ioo

added theorem metric.bounded_of_bdd_above_of_bdd_below

deleted theorem metric.bounded_of_compact

added theorem totally_bounded.bounded

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean