Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 14:24 8addf9a7

View on Github →

feat(topology/bcf): better dist_lt_of_* lemmas (#6781)

Estimated changes

Modified src/topology/bounded_continuous_function.lean

added theorem bounded_continuous_function.dist_le_of_nonempty

added theorem bounded_continuous_function.dist_lt_iff_of_compact

added theorem bounded_continuous_function.dist_lt_iff_of_nonempty_compact

added theorem bounded_continuous_function.dist_lt_of_nonempty_compact

added theorem bounded_continuous_function.norm_lt_iff_of_compact

added theorem bounded_continuous_function.norm_lt_iff_of_nonempty_compact

deleted theorem bounded_continuous_function.norm_lt_of_compact