Ordered pairs

Skip to first unread message

Victor Porton

Mar 6, 2009, 3:22:36 PM3/6/09
to vdash
In a book about ZFC ordered pair <a,b> were defined as something like
{{a}, {a,b}}, so that ordered pair becomes a set.

Please explain the novice in Isabelle whether in Isabelle ordered
pairs are sets. Or what are ordered pairs in Isabelle?

I have an idea of theorem, to prove which I need to show that certain
ordered pairs are not members of certain sets. Could you suggest how
this can be done if <a,b> != {{a}, {a,b}}.

Slawomir Kolodynski

Mar 6, 2009, 6:09:41 PM3/6/09
to vd...@googlegroups.com

This is the definition of ordered pair in ZF.thy:

(* this "symmetric" definition works better than {{a}, {a,b}} *)

Pair_def: "<a,b> == {{a,a}, {a,b}}"

Note you can prove this:

lemma doubleton: shows "{a,a} = {a}"
using singleton_iff Upair_iff by auto;


--- On Fri, 3/6/09, Victor Porton <por...@narod.ru> wrote:

Reply all
Reply to author
0 new messages