:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received July 18, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: ORDINAL2:1
theorem Th2: :: ORDINAL2:2
theorem :: ORDINAL2:3
theorem :: ORDINAL2:4
theorem Th5: :: ORDINAL2:5
:: deftheorem defines last ORDINAL2:def 1 :
theorem :: ORDINAL2:6
canceled;
theorem :: ORDINAL2:7
theorem :: ORDINAL2:8
canceled;
theorem :: ORDINAL2:9
theorem Th10: :: ORDINAL2:10
theorem Th11: :: ORDINAL2:11
theorem :: ORDINAL2:12
canceled;
theorem :: ORDINAL2:13
theorem :: ORDINAL2:14
theorem :: ORDINAL2:15
theorem :: ORDINAL2:16
canceled;
theorem Th17: :: ORDINAL2:17
:: deftheorem ORDINAL2:def 2 :
canceled;
:: deftheorem ORDINAL2:def 3 :
canceled;
:: deftheorem ORDINAL2:def 4 :
canceled;
:: deftheorem ORDINAL2:def 5 :
canceled;
:: deftheorem defines inf ORDINAL2:def 6 :
:: deftheorem Def7 defines sup ORDINAL2:def 7 :
theorem :: ORDINAL2:18
canceled;
theorem :: ORDINAL2:19
canceled;
theorem :: ORDINAL2:20
canceled;
theorem :: ORDINAL2:21
canceled;
theorem :: ORDINAL2:22
theorem :: ORDINAL2:23
theorem :: ORDINAL2:24
theorem :: ORDINAL2:25
theorem Th26: :: ORDINAL2:26
theorem Th27: :: ORDINAL2:27
theorem Th28: :: ORDINAL2:28
theorem :: ORDINAL2:29
theorem :: ORDINAL2:30
theorem :: ORDINAL2:31
theorem :: ORDINAL2:32
:: deftheorem Def8 defines Ordinal-yielding ORDINAL2:def 8 :
theorem :: ORDINAL2:33
canceled;
theorem Th34: :: ORDINAL2:34
:: deftheorem defines sup ORDINAL2:def 9 :
:: deftheorem defines inf ORDINAL2:def 10 :
theorem :: ORDINAL2:35
:: deftheorem defines lim_sup ORDINAL2:def 11 :
:: deftheorem defines lim_inf ORDINAL2:def 12 :
:: deftheorem Def13 defines is_limes_of ORDINAL2:def 13 :
:: deftheorem Def14 defines lim ORDINAL2:def 14 :
:: deftheorem defines lim ORDINAL2:def 15 :
:: deftheorem defines increasing ORDINAL2:def 16 :
:: deftheorem defines continuous ORDINAL2:def 17 :
:: deftheorem Def18 defines +^ ORDINAL2:def 18 :
:: deftheorem Def19 defines *^ ORDINAL2:def 19 :
:: deftheorem Def20 defines exp ORDINAL2:def 20 :
theorem :: ORDINAL2:36
canceled;
theorem :: ORDINAL2:37
canceled;
theorem :: ORDINAL2:38
canceled;
theorem :: ORDINAL2:39
canceled;
theorem :: ORDINAL2:40
canceled;
theorem :: ORDINAL2:41
canceled;
theorem :: ORDINAL2:42
canceled;
theorem :: ORDINAL2:43
canceled;
theorem Th44: :: ORDINAL2:44
theorem Th45: :: ORDINAL2:45
theorem Th46: :: ORDINAL2:46
theorem Th47: :: ORDINAL2:47
Lm1:
1 = succ {}
;
theorem :: ORDINAL2:48
theorem Th49: :: ORDINAL2:49
theorem Th50: :: ORDINAL2:50
theorem Th51: :: ORDINAL2:51
theorem Th52: :: ORDINAL2:52
theorem Th53: :: ORDINAL2:53
theorem Th54: :: ORDINAL2:54
theorem Th55: :: ORDINAL2:55
theorem Th56: :: ORDINAL2:56
theorem Th57: :: ORDINAL2:57
theorem :: ORDINAL2:58
theorem :: ORDINAL2:59
theorem Th60: :: ORDINAL2:60
theorem Th61: :: ORDINAL2:61
theorem Th62: :: ORDINAL2:62
theorem :: ORDINAL2:63
theorem :: ORDINAL2:64
canceled;
theorem :: ORDINAL2:65
:: deftheorem defines is_cofinal_with ORDINAL2:def 21 :
theorem Th66: :: ORDINAL2:66
theorem :: ORDINAL2:67
theorem :: ORDINAL2:68