operator_norm): a few more estimates
#2233

Merged

feat(analysis/normed_space/operator_norm): a few more estimates #2233

mergify merged 9 commits into master from operator-norm

feat(*): a few more theorems about `unique` and `subsingleton`

c44f93a0

Fix compile, fix two non-terminate `simp`s

c8313f0e

Update src/topology/metric_space/antilipschitz.lean

7cde50ef

feat(analysis/normed_space/operator_norm): a few more estimates

f23ed37e

urkud added blocked-by-other-PR

cipher1024 assigned

sgouezel 6 years ago

rename `(anti)lipschitz_with.to_inverse` to `to_right_inverse`

83fdd5e9

Merge branch 'master' into operator-norm

216e747f

urkud removed blocked-by-other-PR

urkud added awaiting-review

sgouezel approved these changes on 2020-03-27

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge branch 'master' into operator-norm

217d90a5

Merge branch 'master' into operator-norm

ce12660a

Merge branch 'master' into operator-norm

d8871340

mergify merged 67327881 into master 6 years ago

urkud deleted the operator-norm branch 6 years ago

Reviewers

sgouezel

Assignees

sgouezel

Labels

ready-to-merge

Milestone

No milestone