Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes