mathlib3
3d457a24 - chore(topology/continuous_function): review API (#9950)

Commit
4 years ago
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(α, β)`.
Author
Parents
Loading