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

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

proof end;

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)

proof end;

registration

cluster Relation-like Function-like constant non empty 1-sorted-yielding for set ;

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is constant & b₁ 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 :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 ) by PRALG_1:def 11;

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 ;

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 for set ;

existence
ex b₁ being 1-sorted-yielding ManySortedSet of I st b₁ 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 -> non-empty ;

coherence
Carrier J is non-empty

proof end;

end;

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 :Def3: :: YELLOW_6:def 3
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 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 & y <= z ) );

registration

let X be set ;

cluster BoolePoset X -> directed ;

coherence
BoolePoset X is directed ;

end;

registration

cluster non empty strict transitive directed for RelStr ;

existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ is directed & b₁ is transitive & b₁ 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;

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 b₁ being RelStr-yielding ManySortedSet of I st b₁ 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 Th3: :: YELLOW_6:3

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 over S;

attr N 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 #) & the mapping of it = the carrier of it --> p );

existence
ex b₁ being strict NetStr over T st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₁ = the carrier of b₁ --> p )

proof end;

correctness
uniqueness
for b₁, b₂ being strict NetStr over T st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₁ = the carrier of b₁ --> p & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₂ = the carrier of b₂ --> p holds
b₁ = b₂;
;

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 b₄ being strict NetStr over T holds
( b₄ = ConstantNet (R,p) iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₄ = the carrier of b₄ --> 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 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

proof end;

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

proof end;

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;

theorem Th6: :: YELLOW_6:6

for R being RelStr holds R is full SubRelStr of R

proof end;

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

proof end;

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 & the mapping of it = the mapping of N | the carrier of it );

existence
ex b₁ being NetStr over S st
( b₁ is SubRelStr of N & the mapping of b₁ = the mapping of N | the carrier of b₁ )

proof end;

end;

:: deftheorem Def6 defines SubNetStr YELLOW_6:def 6 :
for S being 1-sorted
for N, b₃ being NetStr over S holds
( b₃ is SubNetStr of N iff ( b₃ is SubRelStr of N & the mapping of b₃ = the mapping of N | the carrier of b₃ ) );

theorem :: YELLOW_6:8

for S being 1-sorted
for N being NetStr over S holds N is SubNetStr of N

proof end;

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

proof end;

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

proof end;

definition

let S be 1-sorted ;
let N be NetStr over S;
let M be SubNetStr of N;

attr M 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

proof end;

registration

let S be 1-sorted ;
let N be NetStr over S;

cluster strict full for SubNetStr of N;

existence
ex b₁ being SubNetStr of N st
( b₁ is full & b₁ is strict )

proof end;

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 b₁ being SubNetStr of N st
( b₁ is full & not b₁ is empty & b₁ is strict )

proof end;

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

proof end;

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 & y = j & i <= j holds
x <= y

proof end;

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 & y = j & x <= y holds
i <= j

proof end;

registration

let T be non empty 1-sorted ;

cluster non empty transitive strict directed constant for NetStr over T;

existence
ex b₁ being net of T st
( b₁ is constant & b₁ is strict )

proof end;

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 & 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

proof end;

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 & 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

proof end;

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 & ( 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 b₁ being net of T ex f being Function of b₁,N st
( the mapping of b₁ = the mapping of N * f & ( for m being Element of N ex n being Element of b₁ st
for p being Element of b₁ st n <= p holds
m <= f . p ) )

proof end;

end;

:: deftheorem Def9 defines subnet YELLOW_6:def 9 :
for T being non empty 1-sorted
for N, b₃ being net of T holds
( b₃ is subnet of N iff ex f being Function of b₃,N st
( the mapping of b₃ = the mapping of N * f & ( for m being Element of N ex n being Element of b₃ st
for p being Element of b₃ 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

proof end;

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 & N2 is subnet of N3 holds
N1 is subnet of N3

proof end;

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

proof end;

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 & N is_eventually_in Y holds
X meets Y

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let S be 1-sorted ;
let N be NetStr over S;
let X be set ;

func N " X -> strict SubNetStr of N means :Def10: :: YELLOW_6:def 10
( it is full SubRelStr of N & the carrier of it = the mapping of N " X );

existence
ex b₁ being strict SubNetStr of N st
( b₁ is full SubRelStr of N & the carrier of b₁ = the mapping of N " X )

proof end;

uniqueness
for b₁, b₂ being strict SubNetStr of N st b₁ is full SubRelStr of N & the carrier of b₁ = the mapping of N " X & b₂ is full SubRelStr of N & the carrier of b₂ = the mapping of N " X holds
b₁ = b₂

proof end;

end;

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

registration

let S be 1-sorted ;
let N be transitive NetStr over S;
let X be set ;

cluster N " X -> transitive strict full ;

coherence
( N " X is transitive & N " X is full )

proof end;

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 & N " X is directed )

proof end;

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

proof end;

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

proof end;

definition

let X be non empty 1-sorted ;

func NetUniv X -> set means :Def11: :: YELLOW_6:def 11
for x being object 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 b₁ being set st
for x being object holds
( x in b₁ 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 b₁, b₂ being set st ( for x being object holds
( x in b₁ 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 object holds
( x in b₂ iff ex N being strict net of X st
( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines NetUniv YELLOW_6:def 11 :
for X being non empty 1-sorted
for b₂ being set holds
( b₂ = NetUniv X iff for x being object holds
( x in b₂ 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;

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 b₁ being ManySortedSet of X st
for i being set st i in rng b₁ holds
i is net of T

proof end;

end;

:: deftheorem Def12 defines net_set YELLOW_6:def 12 :
for X being set
for T being 1-sorted
for b₃ being ManySortedSet of X holds
( b₃ is net_set of X,T iff for i being set st i in rng b₃ 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 )

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

end;

registration

let X be set ;
let T be 1-sorted ;

cluster -> RelStr-yielding for net_set of X,T;

coherence
for b₁ being net_set of X,T holds b₁ is RelStr-yielding

proof end;

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 b₁ being net_set of the carrier of Y,T holds b₁ is yielding_non-empty_carriers by Def12;

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 for net_set of X,T;

coherence
for b₁ being net_set of X,T holds b₁ is yielding_non-empty_carriers by Def12;

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 b₁ being net_set of X,T st b₁ 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 :Def13: :: YELLOW_6:def 13
( 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 b₁ being strict net of T st
( RelStr(# the carrier of b₁, the InternalRel of b₁ #) = [: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 b₁ . (i,f) = the mapping of (J . i) . (f . i) ) )

proof end;

uniqueness
for b₁, b₂ being strict net of T st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = [: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 b₁ . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b₂, the InternalRel of b₂ #) = [: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 b₂ . (i,f) = the mapping of (J . i) . (f . i) ) holds
b₁ = b₂

proof end;

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 b₄ being strict net of T holds
( b₄ = Iterated J iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = [: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 b₄ . (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 & ( for i being Element of Y holds J . i in NetUniv T ) holds
Iterated J in NetUniv T

proof end;

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)):]

proof end;

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)

proof end;

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 }

proof end;

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 & 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 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 & 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 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 & p in W & W is open )

proof end;

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 & x is open ) )

proof end;

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 )

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;

definition

let T be non empty TopSpace;
let N be net of T;
defpred S₁[ 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 b₁ being Subset of T st
for p being Point of T holds
( p in b₁ iff for V being a_neighborhood of p holds N is_eventually_in V )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for p being Point of T holds
( p in b₁ iff for V being a_neighborhood of p holds N is_eventually_in V ) ) & ( for p being Point of T holds
( p in b₂ iff for V being a_neighborhood of p holds N is_eventually_in V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Lim YELLOW_6:def 15 :
for T being non empty TopSpace
for N being net of T
for b₃ being Subset of T holds
( b₃ = Lim N iff for p being Point of T holds
( p in b₃ 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

proof end;

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

proof end;

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 } & p in Cl S )

proof end;

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 & 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 :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 b₁ being net of T st b₁ is constant holds
b₁ is convergent by Th33;

end;

registration

let T be non empty TopSpace;

cluster non empty transitive strict directed convergent for NetStr over T;

existence
ex b₁ being net of T st
( b₁ is convergent & b₁ 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 :Def17: :: YELLOW_6:def 17
it in Lim N;

existence
ex b₁ being Element of T st b₁ in Lim N by Def16, SUBSET_1:4;
correctness
uniqueness
for b₁, b₂ being Element of T st b₁ in Lim N & b₂ in Lim N holds
b₁ = b₂;
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 b₃ being Element of T holds
( b₃ = lim N iff b₃ 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

proof end;

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

proof end;

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 & ( for Z being subnet of Y holds not p in Lim Z ) )

proof end;

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)

proof end;

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 b₁ being set st b₁ 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 b₂ being set holds
( b₂ is Convergence-Class of S iff b₂ 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 b₁ being Convergence-Class of S holds b₁ is Relation-like

proof end;

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 & p in Lim N ) );

existence
ex b₁ being Convergence-Class of T st
for N being net of T
for p being Point of T holds
( [N,p] in b₁ iff ( N in NetUniv T & p in Lim N ) )

proof end;

uniqueness
for b₁, b₂ being Convergence-Class of T st ( for N being net of T
for p being Point of T holds
( [N,p] in b₁ 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 b₂ iff ( N in NetUniv T & p in Lim N ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines Convergence YELLOW_6:def 19 :
for T being non empty TopSpace
for b₂ being Convergence-Class of T holds
( b₂ = Convergence T iff for N being net of T
for p being Point of T holds
( [N,p] in b₂ 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 :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;

attr C 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;

attr C 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 & 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 :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 & 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 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) & 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 :Def24: :: YELLOW_6:def 24
( 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 b₁ being strict TopStruct st
( the carrier of b₁ = the carrier of S & the topology of b₁ = { 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 b₁, b₂ being strict TopStruct st the carrier of b₁ = the carrier of S & the topology of b₁ = { 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 b₂ = the carrier of S & the topology of b₂ = { 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
b₁ = b₂;
;

end;

:: deftheorem Def24 defines ConvergenceSpace YELLOW_6:def 24 :
for S being non empty 1-sorted
for C being Convergence-Class of S
for b₃ being strict TopStruct holds
( b₃ = ConvergenceSpace C iff ( the carrier of b₃ = the carrier of S & the topology of b₃ = { 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 Th40: :: YELLOW_6:40

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 :: YELLOW_6:def 25
( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) );

end;

:: deftheorem 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) & C is (SUBNETS) & C is (DIVERGENCE) & 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 b₁ being Convergence-Class of T st
( not b₁ is empty & b₁ is topological )

proof end;

end;

registration

let T be non empty 1-sorted ;

cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) for Convergence-Class of T;

coherence
for b₁ being Convergence-Class of T st b₁ is topological holds
( b₁ is (CONSTANTS) & b₁ is (SUBNETS) & b₁ is (DIVERGENCE) & b₁ is (ITERATED_LIMITS) ) ;

cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological for Convergence-Class of T;

coherence
for b₁ being Convergence-Class of T st b₁ is (CONSTANTS) & b₁ is (SUBNETS) & b₁ is (DIVERGENCE) & b₁ is (ITERATED_LIMITS) holds
b₁ is topological ;

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 )

proof end;

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 & N is_often_in S holds
p in S )

proof end;

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 & rng the mapping of N c= S & p in Lim N )

proof end;

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 )

proof end;