Email Gateway (Aug 22 2022 at 09:37): Email Gateway (Aug 22 2022 at 09:37):From: Mandy Martin <tesleft@hotmail.com>
Hi sir,
Every poset is in which every chain has an upper bound has a maximal element => prove every vector space has a basis.
Every poset is in which every chain has an upper bound has a maximal element => prove every connected graph has a spanning tree.
Regards,
Martin Lee
Email Gateway (Aug 22 2022 at 09:38):From: "C. Diekmann" <diekmann@in.tum.de>
Every poset is in which every chain has an upper bound has a maximal element => prove every vector space has a basis.
A straight forward translation (without thinking about what you might
want) to first order logic would be
lemma "∀ poset ∈ {chain ∈ Posets. ∃ u. upper_bound u chain ∧ is_max
u}. ∀ vector_space. has_basis vector_space"
Note that you need to define Posets, upper_bound, is_max, and has_basis.
Also, note that the locally bound poset and vector_space are
completely independent. I guess the way I wrote it down, it is as hard
to show as
lemma "∀ vector_space. has_basis vector_space"
Probably you want to express that the vector_space is constructed
somehow with the poset.
Cornelius
Last updated: Nov 21 2024 at 12:39 UTC