Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-04 15:25 c940e474

View on Github →

chore(topology/continuous_function): remove forget_boundedness (#10612) It is the same as to_continuous_map.

Estimated changes

Modified src/measure_theory/function/lp_space.lean

deleted theorem continuous_map.to_Lp_comp_forget_boundedness

added theorem continuous_map.to_Lp_comp_to_continuous_map

Modified src/topology/continuous_function/bounded.lean

deleted def bounded_continuous_function.forget_boundedness

deleted def bounded_continuous_function.forget_boundedness_add_hom

deleted theorem bounded_continuous_function.forget_boundedness_coe

deleted def bounded_continuous_function.forget_boundedness_linear_map

added def bounded_continuous_function.to_continuous_map_add_hom

added def bounded_continuous_function.to_continuous_map_linear_map

Modified src/topology/continuous_function/compact.lean

deleted theorem bounded_continuous_function.dist_forget_boundedness

added theorem bounded_continuous_function.dist_to_continuous_map

deleted theorem bounded_continuous_function.norm_forget_boundedness_eq

added theorem bounded_continuous_function.norm_to_continuous_map_eq