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


begin

theorem :: YELLOW_6:1
canceled;

theorem :: YELLOW_6:2
canceled;

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

:: deftheorem YELLOW_6:def 1 :
canceled;

:: deftheorem YELLOW_6:def 2 :
canceled;

:: deftheorem defines the_universe_of YELLOW_6:def 3 :
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 :: YELLOW_6:3
canceled;

theorem :: YELLOW_6:4
canceled;

theorem Th5: :: YELLOW_6:5
for T being Universe
for f being Function st dom f in T & rng f c= T holds
product f in T
proof end;

begin

begin

theorem :: YELLOW_6:6
canceled;

theorem :: YELLOW_6:7
canceled;

theorem :: YELLOW_6:8
canceled;

theorem Th9: :: YELLOW_6:9
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)
proof end;

registration
cluster Relation-like Function-like constant non empty 1-sorted-yielding set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is constant & b1 is 1-sorted-yielding )
proof end;
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 :Def4: :: YELLOW_6:def 4
 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 )
proof end;
end;

:: deftheorem Def4 defines yielding_non-empty_carriers YELLOW_6:def 4 :
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 ;
cluster X --> L -> 1-sorted-yielding ;
coherence
X --> L is 1-sorted-yielding
proof end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding yielding_non-empty_carriers set ;
existence
ex b1 being 1-sorted-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proof end;
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
proof end;
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
proof end;
end;

begin

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

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

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

:: deftheorem Def5 defines directed YELLOW_6:def 5 :
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 & y <= z ) );

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

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

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

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

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 func f . m -> Element of N;
coherence
f . m is Element of N
proof end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers set ;
existence
ex b1 being RelStr-yielding ManySortedSet of I st b1 is yielding_non-empty_carriers
proof end;
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
proof end;
end;

theorem :: YELLOW_6:10
canceled;

theorem :: YELLOW_6:11
canceled;

theorem Th12: :: YELLOW_6:12
for R being RelStr holds the carrier of R = the carrier of (R ~)
proof end;

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
proof end;

definition
let S be 1-sorted ;
let N be NetStr of S;
attr N is constant means :Def6: :: YELLOW_6:def 6
 the mapping of N is constant ;
end;

:: deftheorem Def6 defines constant YELLOW_6:def 6 :
for S being 1-sorted
for N being NetStr of 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 of T means :Def7: :: YELLOW_6:def 7
( 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 )
proof end;
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 :
for R being RelStr
for T being non empty 1-sorted
for p being Element of T
for b4 being strict NetStr of 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 #) & 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
proof end;
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
proof end;
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
proof end;
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
proof end;
end;

theorem Th13: :: YELLOW_6:13
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
proof end;

theorem Th14: :: YELLOW_6:14
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
proof end;

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

begin

theorem Th15: :: YELLOW_6:15
for R being RelStr holds R is full SubRelStr of R
proof end;

theorem Th16: :: YELLOW_6:16
for R being RelStr
for S being SubRelStr of R
for T being SubRelStr of S holds T is SubRelStr of R
proof end;

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

:: deftheorem Def8 defines SubNetStr YELLOW_6:def 8 :
for S being 1-sorted
for N, b3 being NetStr of S holds
( b3 is SubNetStr of N iff ( b3 is SubRelStr of N & the mapping of b3 = the mapping of N | the carrier of b3 ) );

theorem :: YELLOW_6:17
for S being 1-sorted
for N being NetStr of S holds N is SubNetStr of N
proof end;

theorem :: YELLOW_6:18
for Q being 1-sorted
for R being NetStr of Q
for S being SubNetStr of R
for T being SubNetStr of S holds T is SubNetStr of R
proof end;

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
proof end;

definition
let S be 1-sorted ;
let N be NetStr of S;
let M be SubNetStr of N;
attr M is full means :Def9: :: YELLOW_6:def 9
M is full SubRelStr of N;
end;

:: deftheorem Def9 defines full YELLOW_6:def 9 :
for S being 1-sorted
for N being NetStr of 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 of S holds NetStr(# the carrier of R, the InternalRel of R, the mapping of R #) is full SubRelStr of R
proof end;

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

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

theorem Th19: :: YELLOW_6:19
for S being 1-sorted
for N being NetStr of S
for M being SubNetStr of N holds the carrier of M c= the carrier of N
proof end;

theorem Th20: :: YELLOW_6:20
for S being 1-sorted
for N being NetStr of S
for M being SubNetStr of N
for x, y being Element of N
for i, j being Element of M st x = i & y = j & i <= j holds
x <= y
proof end;

theorem Th21: :: YELLOW_6:21
for S being 1-sorted
for N being non empty NetStr of 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 & y = j & x <= y holds
i <= j
proof end;

begin

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

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

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

:: deftheorem Def10 defines the_value_of YELLOW_6:def 10 :
for T being non empty 1-sorted
for N being NetStr of T st N is constant & not N is empty holds
the_value_of N = the_value_of the mapping of N;

theorem Th22: :: YELLOW_6:22
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
proof end;

definition
let T be non empty 1-sorted ;
let N be net of T;
canceled;
mode subnet of N -> net of T means :Def12: :: YELLOW_6:def 12
 ex f being Function of it,N st
( the mapping of it = the mapping of N * f & ( 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 & ( 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 ) )
proof end;
end;

:: deftheorem YELLOW_6:def 11 :
canceled;

:: deftheorem Def12 defines subnet YELLOW_6:def 12 :
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 & ( 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:23
for T being non empty 1-sorted
for N being net of T holds N is subnet of N
proof end;

theorem :: YELLOW_6:24
for T being non empty 1-sorted
for N1, N2, N3 being net of T st N1 is subnet of N2 & N2 is subnet of N3 holds
N1 is subnet of N3
proof end;

theorem Th25: :: YELLOW_6:25
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
proof end;

theorem Th26: :: YELLOW_6:26
for L being non empty 1-sorted
for N being net of L
for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
proof end;

theorem Th27: :: YELLOW_6:27
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
proof end;

theorem Th28: :: YELLOW_6:28
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
proof end;

theorem Th29: :: YELLOW_6:29
for S being non empty 1-sorted
for N being net of S holds N is_eventually_in the carrier of S
proof end;

begin

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

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

registration
let S be 1-sorted ;
let N be transitive NetStr of S;
let X be set ;
cluster N " X -> transitive strict full ;
coherence
( N " X is transitive & N " X is full )
proof end;
end;

theorem Th30: :: YELLOW_6:30
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 & N " X is directed )
proof end;

theorem Th31: :: YELLOW_6:31
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
proof end;

theorem Th32: :: YELLOW_6:32
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
proof end;

begin

definition
let X be non empty 1-sorted ;
func NetUniv X -> set means :Def14: :: YELLOW_6:def 14
 for x being set holds
( x in it iff ex N being strict net of X st
( N = x & 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 & the carrier of N in the_universe_of the carrier of X ) )
proof end;
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 & the carrier of N in the_universe_of the carrier of X ) ) ) & ( for x being set holds
( x in b2 iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines NetUniv YELLOW_6:def 14 :
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 & 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
proof end;
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
proof end;

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

begin

definition
let X be set ;
let T be 1-sorted ;
mode net_set of X,T -> ManySortedSet of X means :Def15: :: YELLOW_6:def 15
 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
proof end;
end;

:: deftheorem Def15 defines net_set YELLOW_6:def 15 :
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 Th33: :: YELLOW_6:33
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 )
proof end;

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 func J . i -> net of T;
coherence
J . i is net of T by Th33;
end;

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

registration
let T be 1-sorted ;
let Y be net of T;
cluster -> yielding_non-empty_carriers 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
proof end;
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 & product J is transitive )
proof end;
end;

registration
let X be set ;
let T be 1-sorted ;
cluster -> yielding_non-empty_carriers net_set of X,T;
coherence
for b1 being net_set of X,T holds b1 is yielding_non-empty_carriers
proof end;
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 net_set of X,T;
existence
ex b1 being net_set of X,T st b1 is yielding_non-empty_carriers
proof end;
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 :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) ) )
proof end;
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
proof end;
end;

:: deftheorem Def16 defines Iterated YELLOW_6:def 16 :
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):] & ( 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 b4 . (i,f) = the mapping of (J . i) . (f . i) ) ) );

theorem Th34: :: YELLOW_6:34
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 & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T
proof end;

theorem Th35: :: YELLOW_6:35
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)):]
proof end;

theorem Th36: :: YELLOW_6:36
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)
proof end;

theorem Th37: :: YELLOW_6:37
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 }
proof end;

begin

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

:: deftheorem defines OpenNeighborhoods YELLOW_6:def 17 :
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 & 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
proof end;
end;

theorem Th38: :: YELLOW_6:38
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 & p in W & W is open )
proof end;

theorem Th39: :: YELLOW_6:39
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 & x is open ) )
proof end;

theorem Th40: :: YELLOW_6:40
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 )
proof end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster OpenNeighborhoods p -> transitive directed ;
coherence
( OpenNeighborhoods p is transitive & OpenNeighborhoods p is directed )
proof end;
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 :Def18: :: YELLOW_6:def 18
 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 )
proof end;
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 ) ) & ( 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
proof end;
end;

:: deftheorem Def18 defines Lim YELLOW_6:def 18 :
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 Th41: :: YELLOW_6:41
for T being non empty TopSpace
for N being net of T
for Y being subnet of N holds Lim N c= Lim Y
proof end;

theorem Th42: :: YELLOW_6:42
for T being non empty TopSpace
for N being constant net of T holds the_value_of N in Lim N
proof end;

theorem Th43: :: YELLOW_6:43
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 } & p in Cl S )
proof end;

theorem Th44: :: YELLOW_6:44
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 & q in Lim N holds
p = q )
proof end;

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

definition
let T be non empty TopSpace;
let N be net of T;
attr N is convergent means :Def19: :: YELLOW_6:def 19
 Lim N <> {} ;
end;

:: deftheorem Def19 defines convergent YELLOW_6:def 19 :
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 NetStr of T;
coherence
for b1 being net of T st b1 is constant holds
b1 is convergent
proof end;
end;

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

definition
let T be non empty Hausdorff TopSpace;
let N be convergent net of T;
func lim N -> Element of T means :Def20: :: YELLOW_6:def 20
it in Lim N;
existence
ex b1 being Element of T st b1 in Lim N
proof end;
correctness
uniqueness
for b1, b2 being Element of T st b1 in Lim N & b2 in Lim N holds
b1 = b2;
by REALSET1:15;
end;

:: deftheorem Def20 defines lim YELLOW_6:def 20 :
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:45
for T being non empty Hausdorff TopSpace
for N being constant net of T holds lim N = the_value_of N
proof end;

theorem :: YELLOW_6:46
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
proof end;

theorem Th47: :: YELLOW_6:47
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 & ( for Z being subnet of Y holds not p in Lim Z ) )
proof end;

theorem Th48: :: YELLOW_6:48
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)
proof end;

begin

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

:: deftheorem Def21 defines Convergence-Class YELLOW_6:def 21 :
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 Convergence-Class of S;
coherence
for b1 being Convergence-Class of S holds b1 is Relation-like
proof end;
end;

definition
let T be non empty TopSpace;
func Convergence T -> Convergence-Class of T means :Def22: :: YELLOW_6:def 22
 for N being net of T
for p being Point of T holds
( [N,p] in it iff ( N in NetUniv T & 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 & p in Lim N ) )
proof end;
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 & p in Lim N ) ) ) & ( for N being net of T
for p being Point of T holds
( [N,p] in b2 iff ( N in NetUniv T & p in Lim N ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines Convergence YELLOW_6:def 22 :
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 & p in Lim N ) ) );

definition
let T be non empty 1-sorted ;
let C be Convergence-Class of T;
attr C is (CONSTANTS) means :Def23: :: YELLOW_6:def 23
 for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C;
attr C is (SUBNETS) means :Def24: :: YELLOW_6:def 24
 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;
attr C is (DIVERGENCE) means :Def25: :: YELLOW_6:def 25
 for X being net of T
for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) );
attr C is (ITERATED_LIMITS) means :Def26: :: YELLOW_6:def 26
 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 Def23 defines (CONSTANTS) YELLOW_6:def 23 :
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 Def24 defines (SUBNETS) YELLOW_6:def 24 :
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 Def25 defines (DIVERGENCE) YELLOW_6:def 25 :
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 & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) );

:: deftheorem Def26 defines (ITERATED_LIMITS) YELLOW_6:def 26 :
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) & Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof end;
end;

definition
let S be non empty 1-sorted ;
let C be Convergence-Class of S;
func ConvergenceSpace C -> strict TopStruct means :Def27: :: YELLOW_6:def 27
( the carrier of it = the carrier of S & 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 & 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 } )
proof end;
correctness
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = the carrier of S & 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 } & the carrier of b2 = the carrier of S & 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 Def27 defines ConvergenceSpace YELLOW_6:def 27 :
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 & 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
proof end;
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
proof end;
end;

theorem Th49: :: YELLOW_6:49
for S being non empty 1-sorted
for C being Convergence-Class of S holds C c= Convergence (ConvergenceSpace C)
proof end;

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

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

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

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

theorem Th50: :: YELLOW_6:50
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 )
proof end;

theorem Th51: :: YELLOW_6:51
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 & N is_often_in S holds
p in S )
proof end;

theorem Th52: :: YELLOW_6:52
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 & rng the mapping of N c= S & p in Lim N )
proof end;

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