[FOM] ontology
Freek Wiedijk
freek at cs.kun.nl
Wed Jan 14 17:21:28 EST 2004
>Are the finite ordinals the same mathematical objects as the
>finite cardinals?
In the Mizar world they are!
theorem x is finite Ordinal iff x is finite Cardinal
proof
hereby
assume x is finite Ordinal;
then x is finite & x in omega by CARD_4:7;
hence x is finite Cardinal by CARD_1:65;
end;
thus thesis;
end;
(I couldn't find this as an already proven theorem in the
MML, but it wouldn't surprise me if it was there somewhere
already.)
Freek
More information about the FOM
mailing list