:: Increasing and Continuous Ordinal Sequences
:: by Grzegorz Bancerek
::
:: Received May 31, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
{} in omega
by ORDINAL1:def 12;
Lm2:
omega is limit_ordinal
by ORDINAL1:def 12;
Lm3:
1 = succ {}
;
theorem :: ORDINAL4:1
:: deftheorem Def1 defines ^ ORDINAL4:def 1 :
theorem :: ORDINAL4:2
canceled;
theorem Th3: :: ORDINAL4:3
theorem :: ORDINAL4:4
Lm4:
for fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of fi holds
dom fi <> {}
theorem Th5: :: ORDINAL4:5
theorem Th6: :: ORDINAL4:6
theorem :: ORDINAL4:7
theorem Th8: :: ORDINAL4:8
theorem Th9: :: ORDINAL4:9
theorem Th10: :: ORDINAL4:10
theorem Th11: :: ORDINAL4:11
theorem Th12: :: ORDINAL4:12
theorem Th13: :: ORDINAL4:13
theorem Th14: :: ORDINAL4:14
theorem Th15: :: ORDINAL4:15
theorem Th16: :: ORDINAL4:16
Lm5:
for f, g being Function
for X being set st rng f c= X holds
(g | X) * f = g * f
theorem :: ORDINAL4:17
theorem :: ORDINAL4:18
theorem Th19: :: ORDINAL4:19
theorem Th20: :: ORDINAL4:20
Lm6:
for A being Ordinal st A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp {} ,B ) holds
{} is_limes_of fi
Lm7:
for A being Ordinal st A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp 1,B ) holds
1 is_limes_of fi
Lm8:
for C, A being Ordinal st A <> {} & A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) & ex D being Ordinal st D is_limes_of fi )
theorem Th21: :: ORDINAL4:21
theorem Th22: :: ORDINAL4:22
theorem Th23: :: ORDINAL4:23
theorem Th24: :: ORDINAL4:24
theorem Th25: :: ORDINAL4:25
theorem :: ORDINAL4:26
theorem :: ORDINAL4:27
theorem :: ORDINAL4:28
theorem :: ORDINAL4:29
theorem Th30: :: ORDINAL4:30
theorem :: ORDINAL4:31
theorem :: ORDINAL4:32
:: deftheorem Def2 defines Ordinal ORDINAL4:def 2 :
:: deftheorem Def3 defines Ordinal-Sequence ORDINAL4:def 3 :
:: deftheorem defines 0-element_of ORDINAL4:def 4 :
:: deftheorem defines 1-element_of ORDINAL4:def 5 :
theorem :: ORDINAL4:33
canceled;
theorem :: ORDINAL4:34
canceled;
theorem :: ORDINAL4:35
theorem Th36: :: ORDINAL4:36
theorem Th37: :: ORDINAL4:37
theorem :: ORDINAL4:38
theorem :: ORDINAL4:39
theorem :: ORDINAL4:40