freek 91: triangle inequality

Stream: general

[Eric Rodriguez]

on https://leanprover-community.github.io/100.html#91, we give that the triangle inequality's proof is docs#norm_add_le, but this is actually the tautological statement that "spaces that obey the triangle inequality (with a bit more structure) do indeed obey the triangle inequality". I think we should replace this with something like docs#real.normed_field or at least specialize the statement to R (without the typeclass arguments); cc @Eric Wieser

[Alex J. Best]

Different people have certainly interpreted what "the triangle inequality" means differently for Freek's list, so I don't think we are unique in writing something somewhat tautological for one of the entries, maybe the model that Isabelle chose is nice for this one: http://www.cse.unsw.edu.au/~kleing/top100/#91

[Adam Topaz]

I would second docs#real.normed_field as "the triangle inequality" for Freek's purposes. It illustrates not only that the reals are a normed field, but that we have a general typeclass for such things.

[Adam Topaz]

Maybe throw docs#complex.normed_field in there as well

[Heather Macbeth]

Or docs#pi_Lp.pseudo_emetric_aux, which is where the work seems to be for $\mathbb{R}^n$ :)