begin
theorem
canceled;
theorem
canceled;
:: deftheorem YELLOW_6:def 1 :
canceled;
:: deftheorem YELLOW_6:def 2 :
canceled;
:: deftheorem defines the_universe_of YELLOW_6:def 3 :
theorem
canceled;
theorem
canceled;
theorem Th5:
begin
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
:: deftheorem Def4 defines yielding_non-empty_carriers YELLOW_6:def 4 :
begin
:: 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
canceled;
theorem
canceled;
theorem Th12:
Lm3:
for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of S,the InternalRel of S #) & p <= q holds
p9 <= q9
:: deftheorem Def6 defines constant YELLOW_6:def 6 :
definition
let R be
RelStr ;
let T be non
empty 1-sorted ;
let p be
Element of
T;
func ConstantNet R,
p -> strict NetStr of
T means :
Def7:
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
R,the
InternalRel of
R #) & the
mapping of
it = the
carrier of
it --> p );
existence
ex b1 being strict NetStr of T st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b1 = the carrier of b1 --> p )
correctness
uniqueness
for b1, b2 being strict NetStr of T st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b1 = the carrier of b1 --> p & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b2 = the carrier of b2 --> p holds
b1 = b2;
;
end;
:: deftheorem Def7 defines ConstantNet YELLOW_6:def 7 :
theorem Th13:
theorem Th14:
begin
theorem Th15:
theorem Th16:
:: deftheorem Def8 defines SubNetStr YELLOW_6:def 8 :
theorem
theorem
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:
theorem Th20:
theorem Th21:
begin
:: deftheorem Def10 defines the_value_of YELLOW_6:def 10 :
theorem Th22:
:: deftheorem YELLOW_6:def 11 :
canceled;
:: deftheorem Def12 defines subnet YELLOW_6:def 12 :
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
:: deftheorem Def13 defines " YELLOW_6:def 13 :
theorem Th30:
theorem Th31:
theorem Th32:
begin
:: 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
begin
:: deftheorem Def15 defines net_set YELLOW_6:def 15 :
theorem Th33:
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:
(
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:
theorem Th35:
theorem Th36:
theorem Th37:
begin
:: deftheorem defines OpenNeighborhoods YELLOW_6:def 17 :
theorem Th38:
theorem Th39:
theorem Th40:
begin
:: deftheorem Def18 defines Lim YELLOW_6:def 18 :
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
:: deftheorem Def19 defines convergent YELLOW_6:def 19 :
:: deftheorem Def20 defines lim YELLOW_6:def 20 :
theorem
theorem
theorem Th47:
theorem Th48:
begin
:: 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:
:: deftheorem Def28 defines topological YELLOW_6:def 28 :
theorem Th50:
theorem Th51:
theorem Th52:
theorem