Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.norm_lt_of_compact

Modification history

2021-03-26 14:24
src/topology/bounded_continuous_function.lean
feat(topology/bcf): better dist_lt_of_* lemmas (#6781)
Deleted bounded_continuous_function.norm_lt_of_compactView on Github →
2021-03-04 17:49
src/topology/bounded_continuous_function.lean
feat(bounded_continuous_function): norm_lt_of_compact (#6524)
Added bounded_continuous_function.norm_lt_of_compactView on Github →