:: Chains on a Grating in Euclidean Space
:: by Freek Wiedijk
::
:: Received January 27, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: CHAIN_1:1
theorem Th2: :: CHAIN_1:2
:: deftheorem defines zero CHAIN_1:def 1 :
:: deftheorem Def2 defines zero CHAIN_1:def 2 :
theorem :: CHAIN_1:3
canceled;
theorem Th4: :: CHAIN_1:4
theorem Th5: :: CHAIN_1:5
theorem Th6: :: CHAIN_1:6
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 :: CHAIN_1:7
theorem Th8: :: CHAIN_1:8
theorem Th9: :: CHAIN_1:9
:: deftheorem CHAIN_1:def 3 :
canceled;
:: deftheorem Def4 defines REAL CHAIN_1:def 4 :
:: deftheorem Def5 defines Grating CHAIN_1:def 5 :
theorem Th10: :: CHAIN_1:10
theorem Th11: :: CHAIN_1:11
theorem Th12: :: CHAIN_1:12
theorem Th13: :: CHAIN_1:13
theorem Th14: :: CHAIN_1:14
theorem :: CHAIN_1:15
theorem :: CHAIN_1:16
:: deftheorem Def6 defines Gap CHAIN_1:def 6 :
theorem Th17: :: CHAIN_1:17
for
Gi being non
trivial finite Subset of
REAL 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 :: CHAIN_1:18
deffunc H1( set ) -> set = $1;
theorem Th19: :: CHAIN_1:19
theorem Th20: :: CHAIN_1:20
theorem Th21: :: CHAIN_1:21
theorem Th22: :: CHAIN_1:22
theorem Th23: :: CHAIN_1:23
:: deftheorem defines cell CHAIN_1:def 7 :
theorem Th24: :: CHAIN_1:24
theorem Th25: :: CHAIN_1:25
theorem Th26: :: CHAIN_1:26
theorem Th27: :: CHAIN_1:27
theorem Th28: :: CHAIN_1:28
theorem Th29: :: CHAIN_1:29
theorem Th30: :: CHAIN_1:30
theorem Th31: :: CHAIN_1:31
theorem Th32: :: CHAIN_1:32
:: deftheorem Def8 defines cells CHAIN_1:def 8 :
theorem Th33: :: CHAIN_1:33
theorem Th34: :: CHAIN_1:34
theorem Th35: :: CHAIN_1:35
theorem Th36: :: CHAIN_1:36
theorem :: CHAIN_1:37
theorem Th38: :: CHAIN_1:38
theorem Th39: :: CHAIN_1:39
theorem Th40: :: CHAIN_1:40
theorem Th41: :: CHAIN_1:41
theorem Th42: :: CHAIN_1:42
theorem :: CHAIN_1:43
theorem Th44: :: CHAIN_1:44
theorem :: CHAIN_1:45
theorem Th46: :: CHAIN_1:46
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: :: CHAIN_1:47
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: :: CHAIN_1:48
:: 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:
:: CHAIN_1:def 11
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: :: CHAIN_1:49
theorem Th50: :: CHAIN_1:50
:: deftheorem defines star CHAIN_1:def 12 :
theorem Th51: :: CHAIN_1:51
:: deftheorem defines del CHAIN_1:def 13 :
:: deftheorem defines bounds CHAIN_1:def 14 :
theorem Th52: :: CHAIN_1:52
theorem Th53: :: CHAIN_1:53
theorem Th54: :: CHAIN_1:54
theorem Th55: :: CHAIN_1:55
theorem Th56: :: CHAIN_1:56
theorem :: CHAIN_1:57
theorem :: CHAIN_1:58
theorem :: CHAIN_1:59
canceled;
theorem Th60: :: CHAIN_1:60
theorem Th61: :: CHAIN_1:61
theorem Th62: :: CHAIN_1:62
theorem Th63: :: CHAIN_1:63
theorem Th64: :: CHAIN_1:64
theorem Th65: :: CHAIN_1:65
:: deftheorem Def15 defines Cycle CHAIN_1:def 15 :
theorem Th66: :: CHAIN_1:66
theorem :: CHAIN_1:67
theorem Th68: :: CHAIN_1:68
:: deftheorem defines del CHAIN_1:def 16 :
theorem :: CHAIN_1:69
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:
:: CHAIN_1:def 17
( the
carrier of
it = bool (cells k,G) &
0. it = 0_ k,
G & ( for
A,
B being
Element of
it 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 b1
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 b1
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 b2
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 :: CHAIN_1:70
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 :: CHAIN_1:def 18
for
A being
Element of
(Chains (k + 1),G) 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 (Chains (k + 1),G)
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 (Chains (k + 1),G)
for A' being Chain of (k + 1),G st A = A' holds
b1 . A = del A' ) & ( for A being Element of (Chains (k + 1),G)
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 :