basic.lean): implement reverse triangle inequality
#831

Merged

feat (analysis/normed_space/basic.lean): implement reverse triangle inequality #831

mergify merged 3 commits into leanprover-community:master from jdsalchow:inverse_triangle

implement reverse triangle inequality

865f2c4c

PatrickMassot commented on 2019-03-17

make parameters explicit

52c134f1

cipher1024 assigned

avigad 6 years ago

cipher1024 approved these changes on 2019-04-04

cipher1024 added ready-to-merge

Merge branch 'master' into 'inverse_triangle'

c9200cb8

mergify merged 384c9be2 into master 6 years ago

Reviewers

cipher1024

PatrickMassot

Assignees

avigad

Labels

ready-to-merge

Milestone

No milestone