Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.dist_lt_of_nonempty_compact

Modification history

2021-03-26 14:24
src/topology/bounded_continuous_function.lean
feat(topology/bcf): better dist_lt_of_* lemmas (#6781)
Added bounded_continuous_function.dist_lt_of_nonempty_compactView on Github →