Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-04 17:16 384c9be2

View on Github →

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

  • implement reverse triangle inequality
  • make parameters explicit

Estimated changes

added theorem norm_reverse_triangle'
added theorem norm_reverse_triangle