Zulip Chat Archive

Stream: general

Topic: freek 91: triangle inequality

Eric Rodriguez (Oct 06 2022 at 00:24):

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 (Oct 06 2022 at 15:28):

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 (Oct 06 2022 at 15:58):

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 (Oct 06 2022 at 15:58):

Maybe throw docs#complex.normed_field in there as well

Heather Macbeth (Oct 06 2022 at 16:36):

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

Last updated: Aug 03 2023 at 10:10 UTC