Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 17:49 0690d970

View on Github →

feat(bounded_continuous_function): norm_lt_of_compact (#6524)

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/topology/bounded_continuous_function.lean

added theorem bounded_continuous_function.norm_le_of_nonempty

added theorem bounded_continuous_function.norm_lt_of_compact

Modified src/topology/order.lean