Re: [isabelle] Are the countable sets a ccpo

```On Mar 20, 2015 22:42, "Joachim Breitner" <breitner at kit.edu> wrote:
>
> Hi,
>
> Am Freitag, den 20.03.2015, 16:15 +0100 schrieb Bertram Felgenhauer:
> > Andreas Lochbihler wrote:
> > > I am wondering whether the countable sets ordered by inclusion forms a
> > > chain-complete partial order. In other words: If C is a chain of
countable
> > > sets, is the union of all the sets in C countable again?
> >
> > The answer is no. For example, let C be the least uncountable ordinal
> > number; then all its elements are countable, but their union is C
> > itself, because C is a limit ordinal.
>
> but is C a chain, e.g. totally ordered?
>
> I would say the answer is yes:
> A countable set over 'a can be represented as "nat => 'a", a chain of
> those would be "nat => nat => 'a".

Maybe it should be clarified whether we are talking about countable chains
here, or arbitrary totally ordered sets of sets?

So using any bijection
> "nat => (nat Ã nat)", we can show that there are countable many 'aâs in
> there.
>
> Greetings,
> Joachim
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner

```

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