mathlib3

32bd00f1 - refactor(topology/bounded_continuous_function): structure extending continuous_map (#6521)

refactor(topology/bounded_continuous_function): structure extending continuous_map (#6521) Convert `bounded_continuous_function` from a subtype to a structure extending `continuous_map`, and some minor improvements to `@[simp]` lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>