Commit 2021-03-09 02:15 32bd00f1

View on Github →

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.

Estimated changes

Modified src/topology/bounded_continuous_function.lean

modified def bounded_continuous_function.const

deleted theorem bounded_continuous_function.continuous_evalf

added def bounded_continuous_function.mk_of_bound

added theorem bounded_continuous_function.mk_of_bound_coe

modified def bounded_continuous_function.mk_of_compact

added theorem bounded_continuous_function.mk_of_compact_apply

modified def bounded_continuous_function.mk_of_discrete

added theorem bounded_continuous_function.mk_of_discrete_apply

added structure bounded_continuous_function

deleted def bounded_continuous_function

Modified src/topology/continuous_map.lean

added theorem continuous_map.comp_apply

added theorem continuous_map.comp_coe

added theorem continuous_map.const_apply

added theorem continuous_map.const_coe

added theorem continuous_map.id_apply

added theorem continuous_map.id_coe

added theorem continuous_map.to_fun_eq_coe

Modified src/topology/metric_space/gromov_hausdorff_realized.lean