:: Dickson's lemma
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: DICKSON:1
theorem Th2: :: DICKSON:2
for
n being
Nat holds
n c= n + 1
theorem Th3: :: DICKSON:3
:: deftheorem defines ascending DICKSON:def 1 :
:: deftheorem Def2 defines weakly-ascending DICKSON:def 2 :
theorem Th4: :: DICKSON:4
theorem Th5: :: DICKSON:5
theorem :: DICKSON:6
canceled;
theorem Th7: :: DICKSON:7
theorem Th8: :: DICKSON:8
:: deftheorem Def3 defines quasi_ordered DICKSON:def 3 :
:: deftheorem Def4 defines EqRel DICKSON:def 4 :
theorem Th9: :: DICKSON:9
definition
let R be
RelStr ;
func <=E R -> Relation of
Class (EqRel R) means :
Def5:
:: DICKSON:def 5
for
A,
B being
set holds
(
[A,B] in it iff ex
a,
b being
Element of
R st
(
A = Class (EqRel R),
a &
B = Class (EqRel R),
b &
a <= b ) );
existence
ex b1 being Relation of Class (EqRel R) st
for A, B being set holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )
uniqueness
for b1, b2 being Relation of Class (EqRel R) st ( for A, B being set holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) ) ) & ( for A, B being set holds
( [A,B] in b2 iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines <=E DICKSON:def 5 :
theorem Th10: :: DICKSON:10
theorem :: DICKSON:11
:: deftheorem defines \~ DICKSON:def 6 :
:: deftheorem defines \~ DICKSON:def 7 :
theorem :: DICKSON:12
theorem :: DICKSON:13
theorem :: DICKSON:14
theorem :: DICKSON:15
theorem Th16: :: DICKSON:16
theorem Th17: :: DICKSON:17
theorem Th18: :: DICKSON:18
theorem :: DICKSON:19
:: deftheorem Def8 defines min-classes DICKSON:def 8 :
theorem Th20: :: DICKSON:20
theorem Th21: :: DICKSON:21
theorem Th22: :: DICKSON:22
theorem Th23: :: DICKSON:23
theorem Th24: :: DICKSON:24
theorem :: DICKSON:25
:: deftheorem Def9 defines is_Dickson-basis_of DICKSON:def 9 :
theorem Th26: :: DICKSON:26
theorem Th27: :: DICKSON:27
:: deftheorem Def10 defines Dickson DICKSON:def 10 :
theorem Th28: :: DICKSON:28
theorem Th29: :: DICKSON:29
:: deftheorem Def11 defines mindex DICKSON:def 11 :
:: deftheorem Def12 defines mindex DICKSON:def 12 :
theorem Th30: :: DICKSON:30
theorem Th31: :: DICKSON:31
theorem Th32: :: DICKSON:32
theorem Th33: :: DICKSON:33
theorem Th34: :: DICKSON:34
theorem :: DICKSON:35
:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :
theorem Th36: :: DICKSON:36
theorem Th37: :: DICKSON:37
theorem Th38: :: DICKSON:38
theorem Th39: :: DICKSON:39
theorem Th40: :: DICKSON:40
theorem Th41: :: DICKSON:41
theorem Th42: :: DICKSON:42
theorem Th43: :: DICKSON:43
Lm1:
for p being RelStr-yielding ManySortedSet of {} holds
( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )
:: deftheorem defines NATOrd DICKSON:def 14 :
theorem Th44: :: DICKSON:44
theorem Th45: :: DICKSON:45
theorem Th46: :: DICKSON:46
theorem Th47: :: DICKSON:47
:: deftheorem defines OrderedNAT DICKSON:def 15 :
theorem :: DICKSON:48
theorem Th49: :: DICKSON:49
theorem :: DICKSON:50