Commit 2021-07-20 08:59 15893184

feat(topology/continuous_function/bounded): prove norm_eq_supr_norm (#8288) More precisely we prove both:

• bounded_continuous_function.norm_eq_supr_norm
• continuous_map.norm_eq_supr_norm We also introduce one new definition: bounded_continuous_function.norm_comp.