Proof that \empty is not a vector space

Stream: new members

[Arien Malec]

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]

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

[Arien Malec]

I mean that follows from zero right?

[Arien Malec]

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]

variable [Field F] [AddCommGroup V] [Module F V]

example: Nonempty V := Zero.nonempty

[Eric Wieser]

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

[Arien Malec]

Better:

example: ¬IsEmpty V := not_isEmpty_of_nonempty V