:: Moore-Smith Convergence
:: by Andrzej Trybulec
::
:: Received November 12, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let X be set ;
func the_universe_of X ->  set  equals :: YELLOW_6:def 1
 Tarski-Class (the_transitive-closure_of X);
correctness
coherence
Tarski-Class (the_transitive-closure_of X) is set ;
;
end;

:: deftheorem  defines the_universe_of YELLOW_6:def_1_:_
 for X being set holds the_universe_of X = Tarski-Class (the_transitive-closure_of X);

registration
let X be set ;
cluster the_universe_of X ->  epsilon-transitive Tarski ;
coherence
 ( the_universe_of X is epsilon-transitive & the_universe_of X is Tarski ) ;
end;

registration
let X be set ;
cluster the_universe_of X ->  non empty universal ;
coherence
 ( the_universe_of X is universal & not the_universe_of X is empty ) ;
end;

theorem Th1: :: YELLOW_6:1
for T being Universe
for f being Function st dom f in T & rng f c= T holds
product f in T
proofend;

begin

begin

theorem Th2: :: YELLOW_6:2
for Y being non empty set
for J being 1-sorted-yielding ManySortedSet of Y
for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)
proofend;

registration
cluster Relation-like Function-like constant non empty 1-sorted-yielding for set ;
existence
 ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is 1-sorted-yielding )
proofend;
end;

notation
let J be 1-sorted-yielding Function;
synonym  yielding_non-empty_carriers J for  non-Empty ;
end;

definition
let J be 1-sorted-yielding Function;
redefine attr J is non-Empty  means :Def2: :: YELLOW_6:def 2
 for i being set st i in rng J holds
i is non empty 1-sorted ;
compatibility
 ( J is yielding_non-empty_carriers iff for i being set st i in rng J holds
i is non empty 1-sorted )
proofend;
end;

:: deftheorem Def2 defines yielding_non-empty_carriers YELLOW_6:def_2_:_
 for J being 1-sorted-yielding Function holds
( J is yielding_non-empty_carriers iff for i being set st i in rng J holds
i is non empty 1-sorted );

registration
let X be set ;
let L be 1-sorted ;
clusterX --> L ->  1-sorted-yielding ;
coherence
 X --> L is 1-sorted-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding yielding_non-empty_carriers for set ;
existence
 ex b1 being 1-sorted-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proofend;
end;

registration
let I be non empty set ;
let J be RelStr-yielding ManySortedSet of I;
cluster the carrier of (product J) ->  functional ;
coherence
 the carrier of (product J) is functional
proofend;
end;

registration
let I be set ;
let J be 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of I;
cluster Carrier J -> V2() ;
coherence
 Carrier J is non-empty
proofend;
end;

begin

registration
let T be non empty RelStr ;
let A be lower Subset of T;
clusterA `  ->  upper ;
coherence
 A ` is upper
proofend;
end;

registration
let T be non empty RelStr ;
let A be upper Subset of T;
clusterA `  ->  lower ;
coherence
 A ` is lower
proofend;
end;

definition
let N be non empty RelStr ;
redefine attr N is directed  means :Def3: :: YELLOW_6:def 3
 for x, y being Element of N ex z being Element of N st
( x <= z &amp; y <= z );
compatibility
 ( N is directed iff for x, y being Element of N ex z being Element of N st
( x <= z &amp; y <= z ) )
proofend;
end;

:: deftheorem Def3 defines directed YELLOW_6:def_3_:_
 for N being non empty RelStr holds
( N is directed iff for x, y being Element of N ex z being Element of N st
( x <= z &amp; y <= z ) );

registration
let X be set ;
cluster BoolePoset X ->  directed ;
coherence
 BoolePoset X is directed
proofend;
end;

registration
cluster non empty strict transitive directed for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty &amp; b1 is directed &amp; b1 is transitive &amp; b1 is strict )
proofend;
end;

Lm1:  for N being non empty RelStr holds
( N is directed iff RelStr(# the carrier of N, the InternalRel of N #) is directed )
proofend;

Lm2:  for N being non empty RelStr holds
( N is transitive iff RelStr(# the carrier of N, the InternalRel of N #) is transitive )
proofend;

definition
let M be non empty set ;
let N be non empty RelStr ;
let f be Function of M, the carrier of N;
let m be Element of M;
:: original:.
redefine funcf . m ->  Element of N;
coherence
 f . m is Element of N
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers for set ;
existence
 ex b1 being RelStr-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proofend;
end;

registration
let I be non empty set ;
let J be RelStr-yielding yielding_non-empty_carriers ManySortedSet of I;
cluster product J ->  non empty ;
coherence
 not product J is empty ;
end;

registration
let Y1, Y2 be directed RelStr ;
cluster[:Y1,Y2:] ->  directed ;
coherence
 [:Y1,Y2:] is directed
proofend;
end;

theorem Th3: :: YELLOW_6:3
for R being RelStr holds the carrier of R = the carrier of (R ~)
proofend;

Lm3:  for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 &amp; q = q9 &amp; RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) &amp; p <= q holds
p9 <= q9
proofend;

definition
let S be 1-sorted ;
let N be NetStr over S;
attrN is constant  means :Def4: :: YELLOW_6:def 4
 the mapping of N is constant ;
end;

:: deftheorem Def4 defines constant YELLOW_6:def_4_:_
 for S being 1-sorted
for N being NetStr over S holds
( N is constant iff the mapping of N is constant );

definition
let R be RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
func ConstantNet (R,p) ->  strict NetStr over T means :Def5: :: YELLOW_6:def 5
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of it = the carrier of it --> p );
existence
 ex b1 being strict NetStr over T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b1 = the carrier of b1 --> p )
proofend;
correctness
uniqueness
for b1, b2 being strict NetStr over T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b1 = the carrier of b1 --> p &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b2 = the carrier of b2 --> p holds
b1 = b2;
;
end;

:: deftheorem Def5 defines ConstantNet YELLOW_6:def_5_:_
 for R being RelStr
for T being non empty 1-sorted
for p being Element of T
for b4 being strict NetStr over T holds
( b4 = ConstantNet (R,p) iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) &amp; the mapping of b4 = the carrier of b4 --> p ) );

registration
let R be RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  strict constant ;
coherence
 ConstantNet (R,p) is constant
proofend;
end;

registration
let R be non empty RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  non empty strict ;
coherence
 not ConstantNet (R,p) is empty
proofend;
end;

registration
let R be non empty directed RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  strict directed ;
coherence
 ConstantNet (R,p) is directed
proofend;
end;

registration
let R be non empty transitive RelStr ;
let T be non empty 1-sorted ;
let p be Element of T;
cluster ConstantNet (R,p) ->  transitive strict ;
coherence
 ConstantNet (R,p) is transitive
proofend;
end;

theorem Th4: :: YELLOW_6:4
for R being RelStr
for T being non empty 1-sorted
for p being Element of T holds the carrier of (ConstantNet (R,p)) = the carrier of R
proofend;

theorem Th5: :: YELLOW_6:5
for R being non empty RelStr
for T being non empty 1-sorted
for p being Element of T
for q being Element of (ConstantNet (R,p)) holds (ConstantNet (R,p)) . q = p
proofend;

registration
let T be non empty 1-sorted ;
let N be non empty NetStr over T;
cluster the mapping of N ->  non empty ;
coherence
 not the mapping of N is empty ;
end;

begin

theorem Th6: :: YELLOW_6:6
for R being RelStr holds R is full SubRelStr of R
proofend;

theorem Th7: :: YELLOW_6:7
for R being RelStr
for S being SubRelStr of R
for T being SubRelStr of S holds T is SubRelStr of R
proofend;

definition
let S be 1-sorted ;
let N be NetStr over S;
mode SubNetStr of N ->  NetStr over S means :Def6: :: YELLOW_6:def 6
( it is SubRelStr of N &amp; the mapping of it = the mapping of N | the carrier of it );
existence
 ex b1 being NetStr over S st
( b1 is SubRelStr of N &amp; the mapping of b1 = the mapping of N | the carrier of b1 )
proofend;
end;

:: deftheorem Def6 defines SubNetStr YELLOW_6:def_6_:_
 for S being 1-sorted
for N, b3 being NetStr over S holds
( b3 is SubNetStr of N iff ( b3 is SubRelStr of N &amp; the mapping of b3 = the mapping of N | the carrier of b3 ) );

theorem :: YELLOW_6:8
for S being 1-sorted
for N being NetStr over S holds N is SubNetStr of N
proofend;

theorem :: YELLOW_6:9
for Q being 1-sorted
for R being NetStr over Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
proofend;

Lm4:  for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is SubNetStr of R
proofend;

definition
let S be 1-sorted ;
let N be NetStr over S;
let M be SubNetStr of N;
attrM is full  means :Def7: :: YELLOW_6:def 7
M is full SubRelStr of N;
end;

:: deftheorem Def7 defines full YELLOW_6:def_7_:_
 for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N holds
( M is full iff M is full SubRelStr of N );

Lm5:  for S being 1-sorted
for R being NetStr over S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
proofend;

registration
let S be 1-sorted ;
let N be NetStr over S;
cluster strict full for SubNetStr of N;
existence
 ex b1 being SubNetStr of N st
( b1 is full &amp; b1 is strict )
proofend;
end;

registration
let S be 1-sorted ;
let N be non empty NetStr over S;
cluster non empty strict full for SubNetStr of N;
existence
 ex b1 being SubNetStr of N st
( b1 is full &amp; not b1 is empty &amp; b1 is strict )
proofend;
end;

theorem Th10: :: YELLOW_6:10
for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N holds the carrier of M c= the carrier of N
proofend;

theorem Th11: :: YELLOW_6:11
for S being 1-sorted
for N being NetStr over S
for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i &amp; y = j &amp; i <= j holds
x <= y
proofend;

theorem Th12: :: YELLOW_6:12
for S being 1-sorted
for N being non empty NetStr over S
for M being non empty full SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i &amp; y = j &amp; x <= y holds
i <= j
proofend;

begin

registration
let T be non empty 1-sorted ;
cluster non empty transitive strict directed constant for NetStr over T;
existence
 ex b1 being net of T st
( b1 is constant &amp; b1 is strict )
proofend;
end;

registration
let T be non empty 1-sorted ;
let N be constant NetStr over T;
cluster the mapping of N ->  constant ;
coherence
 the mapping of N is constant by Def4;
end;

definition
let T be non empty 1-sorted ;
let N be NetStr over T;
assume A1: ( N is constant &amp; not N is empty ) ;
func the_value_of N ->  Element of T equals :Def8: :: YELLOW_6:def 8
 the_value_of the mapping of N;
coherence
 the_value_of the mapping of N is Element of T
proofend;
end;

:: deftheorem Def8 defines the_value_of YELLOW_6:def_8_:_
 for T being non empty 1-sorted
for N being NetStr over T st N is constant &amp; not N is empty holds
the_value_of N = the_value_of the mapping of N;

theorem Th13: :: YELLOW_6:13
for R being non empty RelStr
for T being non empty 1-sorted
for p being Element of T holds the_value_of (ConstantNet (R,p)) = p
proofend;

definition
let T be non empty 1-sorted ;
let N be net of T;
mode subnet of N ->  net of T means :Def9: :: YELLOW_6:def 9
 ex f being Function of it,N st
( the mapping of it = the mapping of N * f &amp; ( for m being Element of N ex n being Element of it st
for p being Element of it st n <= p holds
m <= f . p ) );
existence
 ex b1 being net of T ex f being Function of b1,N st
( the mapping of b1 = the mapping of N * f &amp; ( for m being Element of N ex n being Element of b1 st
for p being Element of b1 st n <= p holds
m <= f . p ) )
proofend;
end;

:: deftheorem Def9 defines subnet YELLOW_6:def_9_:_
 for T being non empty 1-sorted
for N, b3 being net of T holds
( b3 is subnet of N iff ex f being Function of b3,N st
( the mapping of b3 = the mapping of N * f &amp; ( for m being Element of N ex n being Element of b3 st
for p being Element of b3 st n <= p holds
m <= f . p ) ) );

theorem :: YELLOW_6:14
for T being non empty 1-sorted
for N being net of T holds N is subnet of N
proofend;

theorem :: YELLOW_6:15
for T being non empty 1-sorted
for N1, N2, N3 being net of T st N1 is subnet of N2 &amp; N2 is subnet of N3 holds
N1 is subnet of N3
proofend;

theorem Th16: :: YELLOW_6:16
for T being non empty 1-sorted
for N being constant net of T
for i being Element of N holds N . i = the_value_of N
proofend;

theorem Th17: :: YELLOW_6:17
for L being non empty 1-sorted
for N being net of L
for X, Y being set st N is_eventually_in X &amp; N is_eventually_in Y holds
X meets Y
proofend;

theorem Th18: :: YELLOW_6:18
for S being non empty 1-sorted
for N being net of S
for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
proofend;

theorem Th19: :: YELLOW_6:19
for S being non empty 1-sorted
for N being net of S
for X being set st N is_eventually_in X holds
N is_often_in X
proofend;

theorem Th20: :: YELLOW_6:20
for S being non empty 1-sorted
for N being net of S holds N is_eventually_in the carrier of S
proofend;

begin

definition
let S be 1-sorted ;
let N be NetStr over S;
let X be set ;
funcN " X ->  strict SubNetStr of N means :Def10: :: YELLOW_6:def 10
( it is full SubRelStr of N &amp; the carrier of it = the mapping of N " X );
existence
 ex b1 being strict SubNetStr of N st
( b1 is full SubRelStr of N &amp; the carrier of b1 = the mapping of N " X )
proofend;
uniqueness
 for b1, b2 being strict SubNetStr of N st b1 is full SubRelStr of N &amp; the carrier of b1 = the mapping of N " X &amp; b2 is full SubRelStr of N &amp; the carrier of b2 = the mapping of N " X holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines " YELLOW_6:def_10_:_
 for S being 1-sorted
for N being NetStr over S
for X being set
for b4 being strict SubNetStr of N holds
( b4 = N " X iff ( b4 is full SubRelStr of N &amp; the carrier of b4 = the mapping of N " X ) );

registration
let S be 1-sorted ;
let N be transitive NetStr over S;
let X be set ;
clusterN " X ->  transitive strict full ;
coherence
 ( N " X is transitive &amp; N " X is full )
proofend;
end;

theorem Th21: :: YELLOW_6:21
for S being non empty 1-sorted
for N being net of S
for X being set st N is_often_in X holds
( not N " X is empty &amp; N " X is directed )
proofend;

theorem Th22: :: YELLOW_6:22
for S being non empty 1-sorted
for N being net of S
for X being set st N is_often_in X holds
N " X is subnet of N
proofend;

theorem Th23: :: YELLOW_6:23
for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
proofend;

begin

definition
let X be non empty 1-sorted ;
func NetUniv X ->  set  means :Def11: :: YELLOW_6:def 11
 for x being set holds
( x in it iff ex N being strict net of X st
( N = x &amp; the carrier of N in the_universe_of the carrier of X ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex N being strict net of X st
( N = x &amp; the carrier of N in the_universe_of the carrier of X ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex N being strict net of X st
( N = x &amp; the carrier of N in the_universe_of the carrier of X ) ) ) &amp; ( for x being set holds
( x in b2 iff ex N being strict net of X st
( N = x &amp; the carrier of N in the_universe_of the carrier of X ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines NetUniv YELLOW_6:def_11_:_
 for X being non empty 1-sorted
for b2 being set holds
( b2 = NetUniv X iff for x being set holds
( x in b2 iff ex N being strict net of X st
( N = x &amp; the carrier of N in the_universe_of the carrier of X ) ) );

registration
let X be non empty 1-sorted ;
cluster NetUniv X ->  non empty ;
coherence
 not NetUniv X is empty
proofend;
end;

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
proofend;

Lm7:  for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
proofend;

begin

definition
let X be set ;
let T be 1-sorted ;
mode net_set of X,T ->  ManySortedSet of X means :Def12: :: YELLOW_6:def 12
 for i being set st i in rng it holds
i is net of T;
existence
 ex b1 being ManySortedSet of X st
for i being set st i in rng b1 holds
i is net of T
proofend;
end;

:: deftheorem Def12 defines net_set YELLOW_6:def_12_:_
 for X being set
for T being 1-sorted
for b3 being ManySortedSet of X holds
( b3 is net_set of X,T iff for i being set st i in rng b3 holds
i is net of T );

theorem Th24: :: YELLOW_6:24
for X being set
for T being 1-sorted
for F being ManySortedSet of X holds
( F is net_set of X,T iff for i being set st i in X holds
F . i is net of T )
proofend;

definition
let X be non empty set ;
let T be 1-sorted ;
let J be net_set of X,T;
let i be Element of X;
:: original:.
redefine funcJ . i ->  net of T;
coherence
 J . i is net of T by Th24;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster  ->  RelStr-yielding for net_set of X,T;
coherence
 for b1 being net_set of X,T holds b1 is RelStr-yielding
proofend;
end;

registration
let T be 1-sorted ;
let Y be net of T;
cluster  ->  yielding_non-empty_carriers for net_set of the carrier of Y,T;
coherence
 for b1 being net_set of the carrier of Y,T holds b1 is yielding_non-empty_carriers
proofend;
end;

registration
let T be non empty 1-sorted ;
let Y be net of T;
let J be net_set of the carrier of Y,T;
cluster product J ->  transitive directed ;
coherence
 ( product J is directed &amp; product J is transitive )
proofend;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster  ->  yielding_non-empty_carriers for net_set of X,T;
coherence
 for b1 being net_set of X,T holds b1 is yielding_non-empty_carriers
proofend;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster Relation-like X -defined Function-like V14(X) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers for net_set of X,T;
existence
 ex b1 being net_set of X,T st b1 is yielding_non-empty_carriers
proofend;
end;

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 :Def13: :: YELLOW_6:def 13
( RelStr(# the carrier of it, the InternalRel of it #) = [:Y,(product J):] &amp; ( for i being Element of Y
for f being Function st i in the carrier of Y &amp; 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):] &amp; ( for i being Element of Y
for f being Function st i in the carrier of Y &amp; f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) )
proofend;
uniqueness
 for b1, b2 being strict net of T st RelStr(# the carrier of b1, the InternalRel of b1 #) = [:Y,(product J):] &amp; ( for i being Element of Y
for f being Function st i in the carrier of Y &amp; f in the carrier of (product J) holds
the mapping of b1 . (i,f) = the mapping of (J . i) . (f . i) ) &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = [:Y,(product J):] &amp; ( for i being Element of Y
for f being Function st i in the carrier of Y &amp; f in the carrier of (product J) holds
the mapping of b2 . (i,f) = the mapping of (J . i) . (f . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines Iterated YELLOW_6:def_13_:_
 for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T
for b4 being strict net of T holds
( b4 = Iterated J iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = [:Y,(product J):] &amp; ( for i being Element of Y
for f being Function st i in the carrier of Y &amp; f in the carrier of (product J) holds
the mapping of b4 . (i,f) = the mapping of (J . i) . (f . i) ) ) );

theorem Th25: :: YELLOW_6:25
for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T st Y in NetUniv T &amp; ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
proofend;

theorem Th26: :: YELLOW_6:26
for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]
proofend;

theorem Th27: :: YELLOW_6:27
for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)
proofend;

theorem Th28: :: YELLOW_6:28
for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T holds rng the mapping of (Iterated J) c= union  {  (rng the mapping of (J . i)) where i is Element of Y : verum  }
proofend;

begin

definition
let T be non empty TopSpace;
let p be Point of T;
func OpenNeighborhoods p ->  RelStr  equals :: YELLOW_6:def 14
(InclPoset  {  V where V is Subset of T : ( p in V &amp; V is open )  }  ) ~ ;
correctness
coherence
(InclPoset  {  V where V is Subset of T : ( p in V &amp; V is open )  }  ) ~ is RelStr ;
;
end;

:: deftheorem  defines OpenNeighborhoods YELLOW_6:def_14_:_
 for T being non empty TopSpace
for p being Point of T holds OpenNeighborhoods p = (InclPoset  {  V where V is Subset of T : ( p in V &amp; V is open )  }  ) ~ ;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster OpenNeighborhoods p ->  non empty ;
coherence
 not OpenNeighborhoods p is empty
proofend;
end;

theorem Th29: :: YELLOW_6:29
for T being non empty TopSpace
for p being Point of T
for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x &amp; p in W &amp; W is open )
proofend;

theorem Th30: :: YELLOW_6:30
for T being non empty TopSpace
for p being Point of T
for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x &amp; x is open ) )
proofend;

theorem Th31: :: YELLOW_6:31
for T being non empty TopSpace
for p being Point of T
for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )
proofend;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster OpenNeighborhoods p ->  transitive directed ;
coherence
 ( OpenNeighborhoods p is transitive &amp; OpenNeighborhoods p is directed )
proofend;
end;

begin

definition
let T be non empty TopSpace;
let N be net of T;
defpred S1[ Point of T] means  for V being a_neighborhood of $1 holds N is_eventually_in V;
func Lim N ->  Subset of T means :Def15: :: YELLOW_6:def 15
 for p being Point of T holds
( p in it iff for V being a_neighborhood of p holds N is_eventually_in V );
existence
 ex b1 being Subset of T st
for p being Point of T holds
( p in b1 iff for V being a_neighborhood of p holds N is_eventually_in V )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for p being Point of T holds
( p in b1 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) &amp; ( for p being Point of T holds
( p in b2 iff for V being a_neighborhood of p holds N is_eventually_in V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines Lim YELLOW_6:def_15_:_
 for T being non empty TopSpace
for N being net of T
for b3 being Subset of T holds
( b3 = Lim N iff for p being Point of T holds
( p in b3 iff for V being a_neighborhood of p holds N is_eventually_in V ) );

theorem Th32: :: YELLOW_6:32
for T being non empty TopSpace
for N being net of T
for Y being subnet of N holds Lim N c= Lim Y
proofend;

theorem Th33: :: YELLOW_6:33
for T being non empty TopSpace
for N being constant net of T holds the_value_of N in Lim N
proofend;

theorem Th34: :: YELLOW_6:34
for T being non empty TopSpace
for N being net of T
for p being Point of T st p in Lim N holds
for d being Element of N ex S being Subset of T st
( S =  {  (N . c) where c is Element of N : d <= c  }  &amp; p in Cl S )
proofend;

theorem Th35: :: YELLOW_6:35
for T being non empty TopSpace holds
( T is Hausdorff iff for N being net of T
for p, q being Point of T st p in Lim N &amp; q in Lim N holds
p = q )
proofend;

registration
let T be non empty Hausdorff TopSpace;
let N be net of T;
cluster Lim N ->  trivial ;
coherence
 Lim N is trivial
proofend;
end;

definition
let T be non empty TopSpace;
let N be net of T;
attrN is convergent  means :Def16: :: YELLOW_6:def 16
 Lim N <> {} ;
end;

:: deftheorem Def16 defines convergent YELLOW_6:def_16_:_
 for T being non empty TopSpace
for N being net of T holds
( N is convergent iff Lim N <> {} );

registration
let T be non empty TopSpace;
cluster non empty transitive directed constant  ->  convergent for NetStr over T;
coherence
 for b1 being net of T st b1 is constant holds
b1 is convergent
proofend;
end;

registration
let T be non empty TopSpace;
cluster non empty transitive strict directed convergent for NetStr over T;
existence
 ex b1 being net of T st
( b1 is convergent &amp; b1 is strict )
proofend;
end;

definition
let T be non empty Hausdorff TopSpace;
let N be convergent net of T;
func lim N ->  Element of T means :Def17: :: YELLOW_6:def 17
it in Lim N;
existence
 ex b1 being Element of T st b1 in Lim N
proofend;
correctness
uniqueness
for b1, b2 being Element of T st b1 in Lim N &amp; b2 in Lim N holds
b1 = b2;
by ZFMISC_1:def_10;
end;

:: deftheorem Def17 defines lim YELLOW_6:def_17_:_
 for T being non empty Hausdorff TopSpace
for N being convergent net of T
for b3 being Element of T holds
( b3 = lim N iff b3 in Lim N );

theorem :: YELLOW_6:36
for T being non empty Hausdorff TopSpace
for N being constant net of T holds lim N = the_value_of N
proofend;

theorem :: YELLOW_6:37
for T being non empty TopSpace
for N being net of T
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
proofend;

theorem Th38: :: YELLOW_6:38
for T being non empty TopSpace
for N being net of T st N in NetUniv T holds
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T &amp; ( for Z being subnet of Y holds not p in Lim Z ) )
proofend;

theorem Th39: :: YELLOW_6:39
for T being non empty TopSpace
for N being net of T
for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
proofend;

begin

definition
let S be non empty 1-sorted ;
mode Convergence-Class of S ->  set  means :Def18: :: YELLOW_6:def 18
it c= [:(NetUniv S), the carrier of S:];
existence
 ex b1 being set st b1 c= [:(NetUniv S), the carrier of S:] ;
end;

:: deftheorem Def18 defines Convergence-Class YELLOW_6:def_18_:_
 for S being non empty 1-sorted
for b2 being set holds
( b2 is Convergence-Class of S iff b2 c= [:(NetUniv S), the carrier of S:] );

registration
let S be non empty 1-sorted ;
cluster  ->  Relation-like for Convergence-Class of S;
coherence
 for b1 being Convergence-Class of S holds b1 is Relation-like
proofend;
end;

definition
let T be non empty TopSpace;
func Convergence T ->  Convergence-Class of T means :Def19: :: YELLOW_6:def 19
 for N being net of T
for p being Point of T holds
( [N,p] in it iff ( N in NetUniv T &amp; p in Lim N ) );
existence
 ex b1 being Convergence-Class of T st
for N being net of T
for p being Point of T holds
( [N,p] in b1 iff ( N in NetUniv T &amp; p in Lim N ) )
proofend;
uniqueness
 for b1, b2 being Convergence-Class of T st ( for N being net of T
for p being Point of T holds
( [N,p] in b1 iff ( N in NetUniv T &amp; p in Lim N ) ) ) &amp; ( for N being net of T
for p being Point of T holds
( [N,p] in b2 iff ( N in NetUniv T &amp; p in Lim N ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines Convergence YELLOW_6:def_19_:_
 for T being non empty TopSpace
for b2 being Convergence-Class of T holds
( b2 = Convergence T iff for N being net of T
for p being Point of T holds
( [N,p] in b2 iff ( N in NetUniv T &amp; p in Lim N ) ) );

definition
let T be non empty 1-sorted ;
let C be Convergence-Class of T;
attrC is (CONSTANTS)  means :Def20: :: YELLOW_6:def 20
 for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C;
attrC is (SUBNETS)  means :Def21: :: YELLOW_6:def 21
 for N being net of T
for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C;
attrC is (DIVERGENCE)  means :Def22: :: YELLOW_6:def 22
 for X being net of T
for p being Element of T st X in NetUniv T &amp; not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T &amp; ( for Z being subnet of Y holds not [Z,p] in C ) );
attrC is (ITERATED_LIMITS)  means :Def23: :: YELLOW_6:def 23
 for X being net of T
for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C;
end;

:: deftheorem Def20 defines (CONSTANTS) YELLOW_6:def_20_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (CONSTANTS) iff for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C );

:: deftheorem Def21 defines (SUBNETS) YELLOW_6:def_21_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (SUBNETS) iff for N being net of T
for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in C );

:: deftheorem Def22 defines (DIVERGENCE) YELLOW_6:def_22_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (DIVERGENCE) iff for X being net of T
for p being Element of T st X in NetUniv T &amp; not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T &amp; ( for Z being subnet of Y holds not [Z,p] in C ) ) );

:: deftheorem Def23 defines (ITERATED_LIMITS) YELLOW_6:def_23_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (ITERATED_LIMITS) iff for X being net of T
for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C );

registration
let T be non empty TopSpace;
cluster Convergence T ->  (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) ;
coherence
 ( Convergence T is (CONSTANTS) &amp; Convergence T is (SUBNETS) &amp; Convergence T is (DIVERGENCE) &amp; Convergence T is (ITERATED_LIMITS) )
proofend;
end;

definition
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
func ConvergenceSpace C ->  strict TopStruct  means :Def24: :: YELLOW_6:def 24
( the carrier of it = the carrier of S &amp; the topology of it =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = the carrier of S &amp; the topology of b1 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  )
proofend;
correctness
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = the carrier of S &amp; the topology of b1 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  &amp; the carrier of b2 = the carrier of S &amp; the topology of b2 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  holds
b1 = b2;
;
end;

:: deftheorem Def24 defines ConvergenceSpace YELLOW_6:def_24_:_
 for S being non empty 1-sorted
for C being Convergence-Class of S
for b3 being strict TopStruct holds
( b3 = ConvergenceSpace C iff ( the carrier of b3 = the carrier of S &amp; the topology of b3 =  {  V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V  }  ) );

registration
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
cluster ConvergenceSpace C ->  non empty strict ;
coherence
 not ConvergenceSpace C is empty
proofend;
end;

registration
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
cluster ConvergenceSpace C ->  strict TopSpace-like ;
coherence
 ConvergenceSpace C is TopSpace-like
proofend;
end;

theorem Th40: :: YELLOW_6:40
for S being non empty 1-sorted
for C being Convergence-Class of S holds C c= Convergence (ConvergenceSpace C)
proofend;

definition
let T be non empty 1-sorted ;
let C be Convergence-Class of T;
attrC is topological  means :Def25: :: YELLOW_6:def 25
( C is (CONSTANTS) &amp; C is (SUBNETS) &amp; C is (DIVERGENCE) &amp; C is (ITERATED_LIMITS) );
end;

:: deftheorem Def25 defines topological YELLOW_6:def_25_:_
 for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is topological iff ( C is (CONSTANTS) &amp; C is (SUBNETS) &amp; C is (DIVERGENCE) &amp; C is (ITERATED_LIMITS) ) );

registration
let T be non empty 1-sorted ;
cluster Relation-like non empty topological for Convergence-Class of T;
existence
 ex b1 being Convergence-Class of T st
( not b1 is empty &amp; b1 is topological )
proofend;
end;

registration
let T be non empty 1-sorted ;
cluster topological  ->  (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) for Convergence-Class of T;
coherence
 for b1 being Convergence-Class of T st b1 is topological holds
( b1 is (CONSTANTS) &amp; b1 is (SUBNETS) &amp; b1 is (DIVERGENCE) &amp; b1 is (ITERATED_LIMITS) ) by Def25;
cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS)  ->  topological for Convergence-Class of T;
coherence
 for b1 being Convergence-Class of T st b1 is (CONSTANTS) &amp; b1 is (SUBNETS) &amp; b1 is (DIVERGENCE) &amp; b1 is (ITERATED_LIMITS) holds
b1 is topological by Def25;
end;

theorem Th41: :: YELLOW_6:41
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
proofend;

theorem Th42: :: YELLOW_6:42
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C &amp; N is_often_in S holds
p in S )
proofend;

theorem Th43: :: YELLOW_6:43
for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C &amp; rng the mapping of N c= S &amp; p in Lim N )
proofend;

theorem :: YELLOW_6:44
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )
proofend;