Commit 2019-11-20 01:38 0744a3a9
View on Github →feat(analysis/normed_space/operator_norm): extension of a uniform continuous function (#1649)
- Extension of a uniform continuous function
- Use characteristic properties of an extended function, instead of the explicit construction
- Add documentation on similar results in the library
- Update src/topology/algebra/uniform_extension.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Travis failed for no reason
- Update uniform_extension.lean
- eliminate
uniform_extension.lean - Update operator_norm.lean
- Update operator_norm.lean
- Remove
M - Fix docstring; extend_zero should be a simp lemma