mathlib3
feat(analysis/normed_space/operator_norm): extension of a uniform continuous function
#1649
Merged
Merged
feat(analysis/normed_space/operator_norm): extension of a uniform continuous function #1649
mergify
merged
15 commits into
leanprover-community:master
from
aceg00:uniform_extension
Extension of a uniform continuous function
32882c74
jcommelin
commented
on 2019-11-05
robertylewis
changed the title
Use characteristic properties of an extended function, instead of the…
09db9d2d
Add documentation on similar results in the library
2f3ab830
sgouezel
commented
on 2019-11-10
Update src/topology/algebra/uniform_extension.lean
6d1f2159
Travis failed for no reason
1a972beb
Update uniform_extension.lean
f337ecea
Merge branch 'master' into uniform_extension
14f3ab26
Merge branch 'uniform_extension' of https://github.com/aceg00/mathlib…
81af6355
eliminate `uniform_extension.lean`
10691b7e
Update operator_norm.lean
e7f1ce6d
aceg00
changed the title
Update operator_norm.lean
cda53f71
Remove `M`
ce492896
Fix docstring; extend_zero should be a simp lemma
eb715c0c
sgouezel
approved these changes
on 2019-11-19
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into uniform_extension
8b14ca9c
Merge branch 'master' into uniform_extension
c1044a84
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub