# Zulip Chat Archive

## Stream: new members

### Topic: Non-type theorems

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

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

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

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

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

#### 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