Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 15:23 8459d0a6

View on Github →

feat(continuous_function/compact): lemmas characterising norm and dist (#7054) Transport lemmas charactering the norm and distance on bounded continuous functions, to continuous maps with compact domain.

Estimated changes

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.dist_le_iff_of_nonempty

deleted theorem bounded_continuous_function.dist_le_of_nonempty

Modified src/topology/continuous_function/compact.lean

added theorem continuous_map.dist_le

added theorem continuous_map.dist_le_iff_of_nonempty

added theorem continuous_map.dist_le_two_norm

added theorem continuous_map.dist_lt_iff

added theorem continuous_map.dist_lt_iff_of_nonempty

added theorem continuous_map.dist_lt_of_nonempty

added theorem continuous_map.norm_le

added theorem continuous_map.norm_le_of_nonempty

added theorem continuous_map.norm_lt_iff

added theorem continuous_map.norm_lt_iff_of_nonempty