begin
theorem Th1:
theorem Th2:
:: deftheorem defines zero CHAIN_1:def 1 :
:: deftheorem Def2 defines zero CHAIN_1:def 2 :
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
for
X being
set holds
(
card X = 2 iff ex
x,
y being
set st
(
x in X &
y in X &
x <> y & ( for
z being
set holds
( not
z in X or
z = x or
z = y ) ) ) )
theorem
theorem Th8:
theorem Th9:
:: deftheorem CHAIN_1:def 3 :
canceled;
:: deftheorem Def4 defines REAL CHAIN_1:def 4 :
begin
:: deftheorem Def5 defines Grating CHAIN_1:def 5 :
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
:: deftheorem Def6 defines Gap CHAIN_1:def 6 :
theorem Th17:
for
Gi being non
trivial finite Subset of
for
li,
ri being
Real holds
(
[li,ri] is
Gap of
Gi iff (
li in Gi &
ri in Gi & ( (
li < ri & ( for
xi being
Real st
xi in Gi &
li < xi holds
not
xi < ri ) ) or (
ri < li & ( for
xi being
Real st
xi in Gi holds
( not
li < xi & not
xi < ri ) ) ) ) ) )
theorem
for
Gi being non
trivial finite Subset of
for
li,
ri,
li',
ri' being
Real st
Gi = {li,ri} holds
(
[li',ri'] is
Gap of
Gi iff ( (
li' = li &
ri' = ri ) or (
li' = ri &
ri' = li ) ) )
deffunc H1( set ) -> set = $1;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem defines cell CHAIN_1:def 7 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def8 defines cells CHAIN_1:def 8 :
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem
theorem Th46:
for
k,
k' being
Element of
NAT for
d being non
zero Element of
NAT for
l,
r,
l',
r' being
Element of
REAL d for
G being
Grating of
d st
k <= d &
k' <= d &
cell l,
r in cells k,
G &
cell l',
r' in cells k',
G &
cell l,
r c= cell l',
r' holds
for
i being
Element of
Seg d holds
( (
l . i = l' . i &
r . i = r' . i ) or (
l . i = l' . i &
r . i = l' . i ) or (
l . i = r' . i &
r . i = r' . i ) or (
l . i <= r . i &
r' . i < l' . i &
r' . i <= l . i &
r . i <= l' . i ) )
theorem Th47:
for
k,
k' being
Element of
NAT for
d being non
zero Element of
NAT for
l,
r,
l',
r' being
Element of
REAL d for
G being
Grating of
d st
k < k' &
k' <= d &
cell l,
r in cells k,
G &
cell l',
r' in cells k',
G &
cell l,
r c= cell l',
r' holds
ex
i being
Element of
Seg d st
( (
l . i = l' . i &
r . i = l' . i ) or (
l . i = r' . i &
r . i = r' . i ) )
theorem Th48:
:: deftheorem defines 0_ CHAIN_1:def 9 :
:: deftheorem defines Omega CHAIN_1:def 10 :
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
func infinite-cell G -> Cell of
d,
G means :
Def11:
ex
l,
r being
Element of
REAL d st
(
it = cell l,
r & ( for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i ) ) );
existence
ex b1 being Cell of d,G ex l, r being Element of REAL d st
( b1 = cell l,r & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )
uniqueness
for b1, b2 being Cell of d,G st ex l, r being Element of REAL d st
( b1 = cell l,r & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) & ex l, r being Element of REAL d st
( b2 = cell l,r & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines infinite-cell CHAIN_1:def 11 :
theorem Th49:
theorem Th50:
scheme
ChainInd{
F1()
-> non
zero Element of
NAT ,
F2()
-> Grating of
F1(),
F3()
-> Element of
NAT ,
F4()
-> Chain of
F3(),
F2(),
P1[
set ] } :
provided
A1:
P1[
0_ F3(),
F2()]
and A2:
for
A being
Cell of
F3(),
F2() st
A in F4() holds
P1[
{A}]
and A3:
for
C1,
C2 being
Chain of
F3(),
F2() st
C1 c= F4() &
C2 c= F4() &
P1[
C1] &
P1[
C2] holds
P1[
C1 + C2]
:: deftheorem defines star CHAIN_1:def 12 :
theorem Th51:
:: deftheorem defines del CHAIN_1:def 13 :
:: deftheorem defines bounds CHAIN_1:def 14 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
theorem
canceled;
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
:: deftheorem Def15 defines Cycle CHAIN_1:def 15 :
theorem Th66:
theorem
theorem Th68:
:: deftheorem defines del CHAIN_1:def 16 :
theorem
begin
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
let k be
Element of
NAT ;
func Chains k,
G -> strict AbGroup means :
Def17:
( the
carrier of
it = bool (cells k,G) &
0. it = 0_ k,
G & ( for
A,
B being
Element of
for
A',
B' being
Chain of
k,
G st
A = A' &
B = B' holds
A + B = A' + B' ) );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = bool (cells k,G) & 0. b1 = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) )
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = bool (cells k,G) & 0. b1 = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) & the carrier of b2 = bool (cells k,G) & 0. b2 = 0_ k,G & ( for A, B being Element of
for A', B' being Chain of k,G st A = A' & B = B' holds
A + B = A' + B' ) holds
b1 = b2
end;
:: deftheorem Def17 defines Chains CHAIN_1:def 17 :
theorem
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
let k be
Element of
NAT ;
func del k,
G -> Homomorphism of
Chains (k + 1),
G,
Chains k,
G means
for
A being
Element of
for
A' being
Chain of
(k + 1),
G st
A = A' holds
it . A = del A';
existence
ex b1 being Homomorphism of Chains (k + 1),G, Chains k,G st
for A being Element of
for A' being Chain of (k + 1),G st A = A' holds
b1 . A = del A'
uniqueness
for b1, b2 being Homomorphism of Chains (k + 1),G, Chains k,G st ( for A being Element of
for A' being Chain of (k + 1),G st A = A' holds
b1 . A = del A' ) & ( for A being Element of
for A' being Chain of (k + 1),G st A = A' holds
b2 . A = del A' ) holds
b1 = b2
end;
:: deftheorem defines del CHAIN_1:def 18 :