Re: [isabelle] [Isabelle] how to translate this into Isabelle language to prove the this

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.