mathlib3

15893184 - feat(topology/continuous_function/bounded): prove `norm_eq_supr_norm` (#8288)

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`.