Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 19:18 4ae81c2f

View on Github →

feat(bounded_continuous_function): transport structure to C(α, β) when α compact (#6701)

Estimated changes

Modified src/topology/algebra/continuous_functions.lean

added theorem continuous_map.mul_coe

added theorem continuous_map.one_coe

added theorem continuous_map.smul_apply

Modified src/topology/bounded_continuous_function.lean

added def bounded_continuous_function.add_equiv_continuous_map_of_compact

added theorem bounded_continuous_function.add_equiv_continuous_map_of_compact_to_equiv

added def bounded_continuous_function.equiv_continuous_map_of_compact

added def bounded_continuous_function.forget_boundedness

added def bounded_continuous_function.forget_boundedness_add_hom

added theorem bounded_continuous_function.forget_boundedness_coe

added def bounded_continuous_function.isometric_continuous_map_of_compact

added theorem bounded_continuous_function.isometric_continuous_map_of_compact_to_isometric

added def bounded_continuous_function.linear_isometry_continuous_map_of_compact

added theorem bounded_continuous_function.linear_isometry_continuous_map_of_compact_to_add_equiv

added theorem bounded_continuous_function.linear_isometry_continuous_map_of_compact_to_equiv