# Zulip Chat Archive

## Stream: new members

### Topic: Proof that \empty is not a vector space

#### Arien Malec (Dec 09 2023 at 19:22):

I'm struggling with the machinery here -- the proof Axler wants is that his formulation of the laws of a vector space are in terms of the existence of `0 \in V`

but \empty has no elements.

In terms of Mathlib, what's the setup? (I'm generally struggling to get an `EmptyCollection`

instance to work with even to play...)

#### Sebastien Gouezel (Dec 09 2023 at 19:28):

It's probably easier to state and prove the equivalent formulation that a vector space is nonempty.

#### Arien Malec (Dec 09 2023 at 19:28):

I mean that follows from `zero`

right?

#### Arien Malec (Dec 09 2023 at 19:29):

The paper proof I had in my head went something like "an arbitrary vector space has a `zero`

but the existence of the `zero`

is a contradiction of the definition of the empty set"

#### Arien Malec (Dec 09 2023 at 19:32):

```
variable [Field F] [AddCommGroup V] [Module F V]
example: Nonempty V := Zero.nonempty
```

#### Eric Wieser (Dec 09 2023 at 19:38):

I think that's precisely the point; the proof (that you posted above)is trivial

#### Arien Malec (Dec 09 2023 at 19:52):

Better:

`example: ¬IsEmpty V := not_isEmpty_of_nonempty V`

Last updated: Dec 20 2023 at 11:08 UTC