mathlib3

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