Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.mk_of_compact_add

Modification history

2022-02-17 00:34
src/topology/continuous_function/bounded.lean
feat(topology/continuous_function/algebra): generalize algebra instances (#12055) …
Added bounded_continuous_function.mk_of_compact_addView on Github →