9 views

Skip to first unread message

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

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

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;

Slawekk

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu