:: Moore-Smith Convergence
:: by Andrzej Trybulec
::
:: Received November 12, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem Def1 defines the_value_of YELLOW_6:def 1 :
theorem :: YELLOW_6:1
canceled;
theorem Th2: :: YELLOW_6:2
:: deftheorem YELLOW_6:def 2 :
canceled;
:: deftheorem defines the_universe_of YELLOW_6:def 3 :
theorem :: YELLOW_6:3
canceled;
theorem :: YELLOW_6:4
canceled;
theorem Th5: :: YELLOW_6:5
theorem :: YELLOW_6:6
canceled;
theorem :: YELLOW_6:7
canceled;
theorem :: YELLOW_6:8
canceled;
theorem Th9: :: YELLOW_6:9
:: deftheorem Def4 defines yielding_non-empty_carriers YELLOW_6:def 4 :
:: deftheorem Def5 defines directed YELLOW_6:def 5 :
Lm1:
for N being non empty RelStr holds
( N is directed iff RelStr(# the carrier of N,the InternalRel of N #) is directed )
Lm2:
for N being non empty RelStr holds
( N is transitive iff RelStr(# the carrier of N,the InternalRel of N #) is transitive )
theorem :: YELLOW_6:10
canceled;
theorem :: YELLOW_6:11
canceled;
theorem Th12: :: YELLOW_6:12
Lm3:
for R, S being RelStr
for p, q being Element of R
for p', q' being Element of S st p = p' & q = q' & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of S,the InternalRel of S #) & p <= q holds
p' <= q'
:: deftheorem Def6 defines constant YELLOW_6:def 6 :
:: deftheorem Def7 defines --> YELLOW_6:def 7 :
theorem Th13: :: YELLOW_6:13
theorem Th14: :: YELLOW_6:14
theorem Th15: :: YELLOW_6:15
theorem Th16: :: YELLOW_6:16
:: deftheorem Def8 defines SubNetStr YELLOW_6:def 8 :
theorem :: YELLOW_6:17
theorem :: YELLOW_6:18
Lm4:
for S being 1-sorted
for R being NetStr of S holds NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is SubNetStr of R
:: deftheorem Def9 defines full YELLOW_6:def 9 :
Lm5:
for S being 1-sorted
for R being NetStr of S holds NetStr(# the carrier of R,the InternalRel of R,the mapping of R #) is full SubRelStr of R
theorem Th19: :: YELLOW_6:19
theorem Th20: :: YELLOW_6:20
theorem Th21: :: YELLOW_6:21
:: deftheorem Def10 defines the_value_of YELLOW_6:def 10 :
theorem Th22: :: YELLOW_6:22
:: deftheorem YELLOW_6:def 11 :
canceled;
:: deftheorem Def12 defines subnet YELLOW_6:def 12 :
theorem :: YELLOW_6:23
theorem :: YELLOW_6:24
theorem Th25: :: YELLOW_6:25
theorem Th26: :: YELLOW_6:26
theorem Th27: :: YELLOW_6:27
theorem Th28: :: YELLOW_6:28
theorem Th29: :: YELLOW_6:29
:: deftheorem Def13 defines " YELLOW_6:def 13 :
theorem Th30: :: YELLOW_6:30
theorem Th31: :: YELLOW_6:31
theorem Th32: :: YELLOW_6:32
:: deftheorem Def14 defines NetUniv YELLOW_6:def 14 :
Lm6:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being constant net of S1 holds N is constant net of S2
Lm7:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
:: deftheorem Def15 defines net_set YELLOW_6:def 15 :
theorem Th33: :: YELLOW_6:33
definition
let T be non
empty 1-sorted ;
let Y be
net of
T;
let J be
net_set of the
carrier of
Y,
T;
func Iterated J -> strict net of
T means :
Def16:
:: YELLOW_6:def 16
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= [:Y,(product J):] & ( for
i being
Element of
Y for
f being
Function st
i in the
carrier of
Y &
f in the
carrier of
(product J) holds
the
mapping of
it . i,
f = the
mapping of
(J . i) . (f . i) ) );
existence
ex b1 being strict net of T st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . i,f = the mapping of (J . i) . (f . i) ) )
uniqueness
for b1, b2 being strict net of T st RelStr(# the carrier of b1,the InternalRel of b1 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b1 . i,f = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b2,the InternalRel of b2 #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b2 . i,f = the mapping of (J . i) . (f . i) ) holds
b1 = b2
end;
:: deftheorem Def16 defines Iterated YELLOW_6:def 16 :
theorem Th34: :: YELLOW_6:34
theorem Th35: :: YELLOW_6:35
theorem Th36: :: YELLOW_6:36
theorem Th37: :: YELLOW_6:37
:: deftheorem defines OpenNeighborhoods YELLOW_6:def 17 :
theorem Th38: :: YELLOW_6:38
theorem Th39: :: YELLOW_6:39
theorem Th40: :: YELLOW_6:40
:: deftheorem Def18 defines Lim YELLOW_6:def 18 :
theorem Th41: :: YELLOW_6:41
theorem Th42: :: YELLOW_6:42
theorem Th43: :: YELLOW_6:43
theorem Th44: :: YELLOW_6:44
:: deftheorem Def19 defines convergent YELLOW_6:def 19 :
:: deftheorem Def20 defines lim YELLOW_6:def 20 :
theorem :: YELLOW_6:45
theorem :: YELLOW_6:46
theorem Th47: :: YELLOW_6:47
theorem Th48: :: YELLOW_6:48
:: deftheorem Def21 defines Convergence-Class YELLOW_6:def 21 :
:: deftheorem Def22 defines Convergence YELLOW_6:def 22 :
:: deftheorem Def23 defines (CONSTANTS) YELLOW_6:def 23 :
:: deftheorem Def24 defines (SUBNETS) YELLOW_6:def 24 :
:: deftheorem Def25 defines (DIVERGENCE) YELLOW_6:def 25 :
:: deftheorem Def26 defines (ITERATED_LIMITS) YELLOW_6:def 26 :
:: deftheorem Def27 defines ConvergenceSpace YELLOW_6:def 27 :
theorem Th49: :: YELLOW_6:49
:: deftheorem Def28 defines topological YELLOW_6:def 28 :
theorem Th50: :: YELLOW_6:50
theorem Th51: :: YELLOW_6:51
theorem Th52: :: YELLOW_6:52
theorem :: YELLOW_6:53