Ordered pairs

[Victor Porton]

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]

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;

Slawekk

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