Zulip Chat Archive

Stream: new members

Topic: Non-type theorems


view this post on Zulip Bjørn Kjos-Hanssen (Nov 30 2020 at 01:24):

I have a result of this form: M(x) is a metric space iff x<1. Here x is some parameter that the space depends on.

I have proved using instance that, under the assumption x<1, I have a metric_space but is there a natural way to prove that something is not a metric space?

Of course, I can just prove that the relevant axiom fails, e.g., triangle inequality, but I wonder if I can then conclude "it's not (or cannot be made into) a metric space"?

view this post on Zulip Bryan Gin-ge Chen (Nov 30 2020 at 01:32):

\not metric_space X is short for metric_space X -> false, i.e. that an instance of metric_space X leads to a contradiction.

edit: I didn't think enough about this, see below!

view this post on Zulip Reid Barton (Nov 30 2020 at 01:55):

It's not very convenient to state this because of how the data and properties of a metric space are bundled together, but you can write something like "there does not exist a metric_space whose distance function equals (blah)".

view this post on Zulip Reid Barton (Nov 30 2020 at 01:55):

If you're just going to prove that the triangle inequality fails directly then it's probably more sensible to just state that instead.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 02:05):

Note that any type can be made into a metric space by just giving it the discrete metric, so metric_space X -> false is probably not what you want.

view this post on Zulip Bjørn Kjos-Hanssen (Nov 30 2020 at 02:14):

@Kevin Buzzard yeah, I didn't mean it literally :upside_down:
@Reid Barton that's exactly what I mean, "there does not exist a metric_space with distance function (blah)". Imagine that for some values of x the triangle inequality fails, for other values the symmetry condition fails...


Last updated: May 14 2021 at 13:24 UTC