mathlib3
0690d970 - feat(bounded_continuous_function): norm_lt_of_compact (#6524)

Commit

4 years ago

feat(bounded_continuous_function): norm_lt_of_compact (#6524) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents