Commit 2023-10-06 14:17 5c40b849

View on Github →

refactor(MetricSpace/Basic): use cobounded more (#7543)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem comap_norm_atTop'

added theorem tendsto_norm_atTop_iff_cobounded'

added theorem tendsto_norm_cobounded_atTop'

modified theorem tendsto_norm_cocompact_atTop'

Modified Mathlib/Topology/Bornology/Basic.lean

Modified Mathlib/Topology/Instances/Int.lean

added theorem Int.cobounded_eq

Modified Mathlib/Topology/Instances/Real.lean

added theorem Real.cobounded_eq

Modified Mathlib/Topology/MetricSpace/Basic.lean

added theorem Metric.cobounded_eq_cocompact

added theorem Metric.cobounded_le_cocompact

added theorem Metric.comap_dist_left_atTop

added theorem Metric.comap_dist_right_atTop

added theorem Metric.hasBasis_cobounded_compl_ball

added theorem Metric.hasBasis_cobounded_compl_closedBall

added theorem Metric.isBounded_iff_subset_ball

added theorem Metric.tendsto_dist_left_atTop_iff

added theorem Metric.tendsto_dist_left_cobounded_atTop

added theorem Metric.tendsto_dist_right_atTop_iff

added theorem Metric.tendsto_dist_right_cobounded_atTop

deleted theorem comap_dist_left_atTop_le_cocompact

deleted theorem comap_dist_right_atTop_eq_cocompact

deleted theorem comap_dist_right_atTop_le_cocompact