Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 13:43 3d457a24

View on Github →

chore(topology/continuous_function): review API (#9950)

add simps config for α →ᵇ β;
use better variable names in topology.continuous_function.compact;
weaken some TC assumptions in topology.continuous_function.compact;
migrate more API from α →ᵇ β to C(α, β).

Estimated changes

Modified src/topology/continuous_function/bounded.lean

deleted theorem bounded_continuous_function.coe_const

modified def bounded_continuous_function.const

added theorem bounded_continuous_function.const_apply'

deleted theorem bounded_continuous_function.const_apply

modified def bounded_continuous_function.mk_of_discrete

deleted theorem bounded_continuous_function.mk_of_discrete_apply

added def bounded_continuous_function.simps.apply

Modified src/topology/continuous_function/compact.lean

added theorem bounded_continuous_function.dist_forget_boundedness

added theorem bounded_continuous_function.dist_mk_of_compact

modified theorem bounded_continuous_function.norm_forget_boundedness_eq

added theorem bounded_continuous_function.norm_mk_of_compact

modified def continuous_map.add_equiv_bounded_of_compact

deleted theorem continuous_map.add_equiv_bounded_of_compact_apply_apply

deleted theorem continuous_map.add_equiv_bounded_of_compact_to_equiv

added theorem continuous_map.continuous_coe

added theorem continuous_map.continuous_eval

added theorem continuous_map.continuous_evalx

added theorem continuous_map.dist_apply_le_dist

modified theorem continuous_map.dist_lt_of_nonempty

modified def continuous_map.equiv_bounded_of_compact

modified theorem continuous_map.linear_isometry_bounded_of_compact_apply_apply

modified theorem continuous_map.linear_isometry_bounded_of_compact_symm_apply

Modified src/topology/continuous_function/stone_weierstrass.lean