Re: [isabelle] Are the countable sets a ccpo
On Mar 20, 2015 22:42, "Joachim Breitner" <breitner at kit.edu> wrote:
> 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
> > > 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
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
This archive was generated by a fusion of
Pipermail (Mailman edition) and