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