Non-type theorems

Stream: new members

[Bjørn Kjos-Hanssen]

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"?

[Bryan Gin-ge Chen]

\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!

[Reid Barton]

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)".

[Reid Barton]

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

[Kevin Buzzard]

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.

[Bjørn Kjos-Hanssen]

@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...