Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.norm_le_of_nonempty

Modification history

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_le_of_nonemptyView on Github →