:: by Andrzej Trybulec

::

:: Received November 12, 1996

:: Copyright (c) 1996-2018 Association of Mizar Users

definition
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);

for X being set holds the_universe_of X = Tarski-Class (the_transitive-closure_of X);

registration

let X be set ;

coherence

( the_universe_of X is epsilon-transitive & the_universe_of X is Tarski ) ;

end;
coherence

( the_universe_of X is epsilon-transitive & the_universe_of X is Tarski ) ;

registration
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)

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

existence

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is constant & b_{1} is 1-sorted-yielding )

end;
ex b

( not b

proof end;

notation
end;

definition

let J be 1-sorted-yielding Function;

( J is yielding_non-empty_carriers iff for i being set st i in rng J holds

i is non empty 1-sorted )

end;
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 for i being set st i in rng J holds

i is non empty 1-sorted ;

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

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

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

registration

let I be set ;

ex b_{1} being 1-sorted-yielding ManySortedSet of I st b_{1} is yielding_non-empty_carriers

end;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding yielding_non-empty_carriers for ManySortedSet of ;

existence ex b

proof end;

registration

let I be non empty set ;

let J be RelStr-yielding ManySortedSet of I;

coherence

the carrier of (product J) is functional

end;
let J be RelStr-yielding ManySortedSet of I;

coherence

the carrier of (product J) is functional

proof end;

registration

let I be set ;

let J be 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of I;

coherence

Carrier J is non-empty

end;
let J be 1-sorted-yielding yielding_non-empty_carriers ManySortedSet of I;

coherence

Carrier J is non-empty

proof end;

registration
end;

registration
end;

definition

let N be non empty RelStr ;

( N is directed iff for x, y being Element of N ex z being Element of N st

( x <= z & y <= z ) )

end;
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 for x, y being Element of N ex z being Element of N st

( x <= z & y <= z );

( N is directed iff for x, y being Element of N ex z being Element of N st

( x <= z & y <= z ) )

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

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

registration

existence

ex b_{1} being RelStr st

( not b_{1} is empty & b_{1} is directed & b_{1} is transitive & b_{1} is strict )

end;
ex b

( not b

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

ex b_{1} being RelStr-yielding ManySortedSet of I st b_{1} is yielding_non-empty_carriers

end;
cluster Relation-like I -defined Function-like V14(I) 1-sorted-yielding RelStr-yielding yielding_non-empty_carriers for ManySortedSet of ;

existence ex b

proof end;

registration

let I be non empty set ;

let J be RelStr-yielding yielding_non-empty_carriers ManySortedSet of I;

coherence

not product J is empty ;

end;
let J be RelStr-yielding yielding_non-empty_carriers ManySortedSet of I;

coherence

not product J is empty ;

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;

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

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;

ex b_{1} being strict NetStr over T st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{1} = the carrier of b_{1} --> p )

uniqueness

for b_{1}, b_{2} being strict NetStr over T st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{1} = the carrier of b_{1} --> p & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{2} = the carrier of b_{2} --> p holds

b_{1} = b_{2};

;

end;
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 ( 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 );

ex b

( RelStr(# the carrier of b

proof end;

correctness uniqueness

for b

b

;

:: 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_{4} being strict NetStr over T holds

( b_{4} = ConstantNet (R,p) iff ( RelStr(# the carrier of b_{4}, the InternalRel of b_{4} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{4} = the carrier of b_{4} --> p ) );

for R being RelStr

for T being non empty 1-sorted

for p being Element of T

for b

( b

registration

let R be RelStr ;

let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is constant

end;
let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is constant

proof end;

registration

let R be non empty RelStr ;

let T be non empty 1-sorted ;

let p be Element of T;

coherence

not ConstantNet (R,p) is empty

end;
let T be non empty 1-sorted ;

let p be Element of T;

coherence

not ConstantNet (R,p) is empty

proof end;

registration

let R be non empty directed RelStr ;

let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is directed

end;
let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is directed

proof end;

registration

let R be non empty transitive RelStr ;

let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is transitive

end;
let T be non empty 1-sorted ;

let p be Element of T;

coherence

ConstantNet (R,p) is transitive

proof 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

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

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;

coherence

not the mapping of N is empty ;

end;
let N be non empty NetStr over T;

coherence

not the mapping of N is empty ;

definition

let S be 1-sorted ;

let N be NetStr over S;

ex b_{1} being NetStr over S st

( b_{1} is SubRelStr of N & the mapping of b_{1} = the mapping of N | the carrier of b_{1} )

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

ex b

( b

proof end;

:: deftheorem Def6 defines SubNetStr YELLOW_6:def 6 :

for S being 1-sorted

for N, b_{3} being NetStr over S holds

( b_{3} is SubNetStr of N iff ( b_{3} is SubRelStr of N & the mapping of b_{3} = the mapping of N | the carrier of b_{3} ) );

for S being 1-sorted

for N, b

( b

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

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;

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

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;

existence

ex b_{1} being SubNetStr of N st

( b_{1} is full & b_{1} is strict )

end;
let N be NetStr over S;

existence

ex b

( b

proof end;

registration

let S be 1-sorted ;

let N be non empty NetStr over S;

existence

ex b_{1} being SubNetStr of N st

( b_{1} is full & not b_{1} is empty & b_{1} is strict )

end;
let N be non empty NetStr over S;

existence

ex b

( b

proof 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

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

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

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 ;

existence

ex b_{1} being net of T st

( b_{1} is constant & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let T be non empty 1-sorted ;

let N be constant NetStr over T;

coherence

the mapping of N is constant by Def4;

end;
let N be constant NetStr over T;

coherence

the mapping of N is constant by Def4;

definition

let T be non empty 1-sorted ;

let N be NetStr over T;

assume A1: ( N is constant & not N is empty ) ;

coherence

the_value_of the mapping of N is Element of T

end;
let N be NetStr over T;

assume A1: ( N is constant & not N is empty ) ;

coherence

the_value_of the mapping of N is Element of T

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

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

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;

ex b_{1} being net of T ex f being Function of b_{1},N st

( the mapping of b_{1} = the mapping of N * f & ( for m being Element of N ex n being Element of b_{1} st

for p being Element of b_{1} st n <= p holds

m <= f . p ) )

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

ex b

( the mapping of b

for p being Element of b

m <= f . p ) )

proof end;

:: deftheorem Def9 defines subnet YELLOW_6:def 9 :

for T being non empty 1-sorted

for N, b_{3} being net of T holds

( b_{3} is subnet of N iff ex f being Function of b_{3},N st

( the mapping of b_{3} = the mapping of N * f & ( for m being Element of N ex n being Element of b_{3} st

for p being Element of b_{3} st n <= p holds

m <= f . p ) ) );

for T being non empty 1-sorted

for N, b

( b

( the mapping of b

for p being Element of b

m <= f . p ) ) );

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

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

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

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

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

for N being net of S

for X being set st N is_eventually_in X holds

N is_often_in X

proof end;

definition

let S be 1-sorted ;

let N be NetStr over S;

let X be set ;

ex b_{1} being strict SubNetStr of N st

( b_{1} is full SubRelStr of N & the carrier of b_{1} = the mapping of N " X )

for b_{1}, b_{2} being strict SubNetStr of N st b_{1} is full SubRelStr of N & the carrier of b_{1} = the mapping of N " X & b_{2} is full SubRelStr of N & the carrier of b_{2} = the mapping of N " X holds

b_{1} = b_{2}

end;
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 ( it is full SubRelStr of N & the carrier of it = the mapping of N " X );

ex b

( b

proof end;

uniqueness for b

b

proof 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_{4} being strict SubNetStr of N holds

( b_{4} = N " X iff ( b_{4} is full SubRelStr of N & the carrier of b_{4} = the mapping of N " X ) );

for S being 1-sorted

for N being NetStr over S

for X being set

for b

( b

registration

let S be 1-sorted ;

let N be transitive NetStr over S;

let X be set ;

coherence

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

end;
let N be transitive NetStr over S;

let X be set ;

coherence

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

proof 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 )

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

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

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 ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex N being strict net of X st

( N = x & the carrier of N in the_universe_of the carrier of X ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for x being object holds

( x in b

( N = x & the carrier of N in the_universe_of the carrier of X ) )

proof end;

uniqueness for b

( x in b

( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) & ( for x being object holds

( x in b

( N = x & the carrier of N in the_universe_of the carrier of X ) ) ) holds

b

proof end;

:: deftheorem Def11 defines NetUniv YELLOW_6:def 11 :

for X being non empty 1-sorted

for b_{2} being set holds

( b_{2} = NetUniv X iff for x being object holds

( x in b_{2} 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 non empty 1-sorted

for b

( b

( x in b

( N = x & the carrier of N in the_universe_of the carrier of X ) ) );

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 ;

ex b_{1} being ManySortedSet of X st

for i being set st i in rng b_{1} holds

i is net of T

end;
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 for i being set st i in rng it holds

i is net of T;

ex b

for i being set st i in rng b

i is net of T

proof end;

:: deftheorem Def12 defines net_set YELLOW_6:def 12 :

for X being set

for T being 1-sorted

for b_{3} being ManySortedSet of X holds

( b_{3} is net_set of X,T iff for i being set st i in rng b_{3} holds

i is net of T );

for X being set

for T being 1-sorted

for b

( b

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 )

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

registration

let X be set ;

let T be 1-sorted ;

coherence

for b_{1} being net_set of X,T holds b_{1} is RelStr-yielding

end;
let T be 1-sorted ;

coherence

for b

proof end;

registration

let T be 1-sorted ;

let Y be net of T;

coherence

for b_{1} being net_set of the carrier of Y,T holds b_{1} is yielding_non-empty_carriers
by Def12;

end;
let Y be net of T;

coherence

for b

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;

coherence

( product J is directed & product J is transitive )

end;
let Y be net of T;

let J be net_set of the carrier of Y,T;

coherence

( product J is directed & product J is transitive )

proof end;

registration

let X be set ;

let T be 1-sorted ;

coherence

for b_{1} being net_set of X,T holds b_{1} is yielding_non-empty_carriers
by Def12;

end;
let T be 1-sorted ;

coherence

for b

registration

let X be set ;

let T be 1-sorted ;

ex b_{1} being net_set of X,T st b_{1} is yielding_non-empty_carriers

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

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

ex b_{1} being strict net of T st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = [: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_{1} . (i,f) = the mapping of (J . i) . (f . i) ) )

for b_{1}, b_{2} being strict net of T st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = [: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_{1} . (i,f) = the mapping of (J . i) . (f . i) ) & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = [: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_{2} . (i,f) = the mapping of (J . i) . (f . i) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( RelStr(# the carrier of b

for f being Function st i in the carrier of Y & f in the carrier of (product J) holds

the mapping of b

proof end;

uniqueness for b

for f being Function st i in the carrier of Y & f in the carrier of (product J) holds

the mapping of b

for f being Function st i in the carrier of Y & f in the carrier of (product J) holds

the mapping of b

b

proof 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_{4} being strict net of T holds

( b_{4} = Iterated J iff ( RelStr(# the carrier of b_{4}, the InternalRel of b_{4} #) = [: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_{4} . (i,f) = the mapping of (J . i) . (f . i) ) ) );

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

( b

for f being Function st i in the carrier of Y & f in the carrier of (product J) holds

the mapping of b

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

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

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)

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 }

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;

coherence

(InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) ~ is RelStr ;

;

end;
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 (InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) ~ ;

coherence

(InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) ~ is RelStr ;

;

:: 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 ) } ) ~ ;

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;

coherence

not OpenNeighborhoods p is empty

end;
let p be Point of T;

coherence

not OpenNeighborhoods p is empty

proof 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 )

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

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 )

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;

coherence

( OpenNeighborhoods p is transitive & OpenNeighborhoods p is directed )

end;
let p be Point of T;

coherence

( OpenNeighborhoods p is transitive & OpenNeighborhoods p is directed )

proof end;

definition

let T be non empty TopSpace;

let N be net of T;

defpred S_{1}[ Point of T] means for V being a_neighborhood of $1 holds N is_eventually_in V;

ex b_{1} being Subset of T st

for p being Point of T holds

( p in b_{1} iff for V being a_neighborhood of p holds N is_eventually_in V )

for b_{1}, b_{2} being Subset of T st ( for p being Point of T holds

( p in b_{1} iff for V being a_neighborhood of p holds N is_eventually_in V ) ) & ( for p being Point of T holds

( p in b_{2} iff for V being a_neighborhood of p holds N is_eventually_in V ) ) holds

b_{1} = b_{2}

end;
let N be net of T;

defpred S

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 for p being Point of T holds

( p in it iff for V being a_neighborhood of p holds N is_eventually_in V );

ex b

for p being Point of T holds

( p in b

proof end;

uniqueness for b

( p in b

( p in b

b

proof end;

:: deftheorem Def15 defines Lim YELLOW_6:def 15 :

for T being non empty TopSpace

for N being net of T

for b_{3} being Subset of T holds

( b_{3} = Lim N iff for p being Point of T holds

( p in b_{3} iff for V being a_neighborhood of p holds N is_eventually_in V ) );

for T being non empty TopSpace

for N being net of T

for b

( b

( p in b

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 )

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 )

( 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
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 <> {} );

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;

coherence

for b_{1} being net of T st b_{1} is constant holds

b_{1} is convergent
by Th33;

end;
coherence

for b

b

registration

let T be non empty TopSpace;

existence

ex b_{1} being net of T st

( b_{1} is convergent & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition

let T be non empty Hausdorff TopSpace;

let N be convergent net of T;

existence

ex b_{1} being Element of T st b_{1} in Lim N
by Def16, SUBSET_1:4;

correctness

uniqueness

for b_{1}, b_{2} being Element of T st b_{1} in Lim N & b_{2} in Lim N holds

b_{1} = b_{2};

by ZFMISC_1:def 10;

end;
let N be convergent net of T;

existence

ex b

correctness

uniqueness

for b

b

by ZFMISC_1:def 10;

:: deftheorem Def17 defines lim YELLOW_6:def 17 :

for T being non empty Hausdorff TopSpace

for N being convergent net of T

for b_{3} being Element of T holds

( b_{3} = lim N iff b_{3} in Lim N );

for T being non empty Hausdorff TopSpace

for N being convergent net of T

for b

( b

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

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

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)

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 ;

ex b_{1} being set st b_{1} c= [:(NetUniv S), the carrier of S:]
;

end;
mode Convergence-Class of S -> set means :Def18: :: YELLOW_6:def 18

it c= [:(NetUniv S), the carrier of S:];

existence it c= [:(NetUniv S), the carrier of S:];

ex b

:: deftheorem Def18 defines Convergence-Class YELLOW_6:def 18 :

for S being non empty 1-sorted

for b_{2} being set holds

( b_{2} is Convergence-Class of S iff b_{2} c= [:(NetUniv S), the carrier of S:] );

for S being non empty 1-sorted

for b

( b

registration

let S be non empty 1-sorted ;

coherence

for b_{1} being Convergence-Class of S holds b_{1} is Relation-like

end;
coherence

for b

proof end;

definition

let T be non empty TopSpace;

ex b_{1} being Convergence-Class of T st

for N being net of T

for p being Point of T holds

( [N,p] in b_{1} iff ( N in NetUniv T & p in Lim N ) )

for b_{1}, b_{2} being Convergence-Class of T st ( for N being net of T

for p being Point of T holds

( [N,p] in b_{1} 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_{2} iff ( N in NetUniv T & p in Lim N ) ) ) holds

b_{1} = b_{2}

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

ex b

for N being net of T

for p being Point of T holds

( [N,p] in b

proof end;

uniqueness for b

for p being Point of T holds

( [N,p] in b

for p being Point of T holds

( [N,p] in b

b

proof end;

:: deftheorem Def19 defines Convergence YELLOW_6:def 19 :

for T being non empty TopSpace

for b_{2} being Convergence-Class of T holds

( b_{2} = Convergence T iff for N being net of T

for p being Point of T holds

( [N,p] in b_{2} iff ( N in NetUniv T & p in Lim N ) ) );

for T being non empty TopSpace

for b

( b

for p being Point of T holds

( [N,p] in b

definition

let T be non empty 1-sorted ;

let C be Convergence-Class of T;

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

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;

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

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

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

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

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;

coherence

( Convergence T is (CONSTANTS) & Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )

end;
coherence

( Convergence T is (CONSTANTS) & Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )

proof end;

definition

let S be non empty 1-sorted ;

let C be Convergence-Class of S;

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = the carrier of S & the topology of b_{1} = { 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 } )

uniqueness

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = the carrier of S & the topology of b_{1} = { 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_{2} = the carrier of S & the topology of b_{2} = { 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_{1} = b_{2};

;

end;
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 ( 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 } );

ex b

( the carrier of b

for N being net of S st [N,p] in C holds

N is_eventually_in V } )

proof end;

correctness uniqueness

for b

for N being net of S st [N,p] in C holds

N is_eventually_in V } & the carrier of b

for N being net of S st [N,p] in C holds

N is_eventually_in V } holds

b

;

:: deftheorem Def24 defines ConvergenceSpace YELLOW_6:def 24 :

for S being non empty 1-sorted

for C being Convergence-Class of S

for b_{3} being strict TopStruct holds

( b_{3} = ConvergenceSpace C iff ( the carrier of b_{3} = the carrier of S & the topology of b_{3} = { 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 } ) );

for S being non empty 1-sorted

for C being Convergence-Class of S

for b

( b

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;

coherence

not ConvergenceSpace C is empty

end;
let C be Convergence-Class of S;

coherence

not ConvergenceSpace C is empty

proof end;

registration

let S be non empty 1-sorted ;

let C be Convergence-Class of S;

coherence

ConvergenceSpace C is TopSpace-like

end;
let C be Convergence-Class of S;

coherence

ConvergenceSpace C is TopSpace-like

proof 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)

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;

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

( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) );

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

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 ;

existence

ex b_{1} being Convergence-Class of T st

( not b_{1} is empty & b_{1} is topological )

end;
existence

ex b

( not b

proof end;

registration

let T be non empty 1-sorted ;

for b_{1} being Convergence-Class of T st b_{1} is topological holds

( b_{1} is (CONSTANTS) & b_{1} is (SUBNETS) & b_{1} is (DIVERGENCE) & b_{1} is (ITERATED_LIMITS) )
;

for b_{1} being Convergence-Class of T st b_{1} is (CONSTANTS) & b_{1} is (SUBNETS) & b_{1} is (DIVERGENCE) & b_{1} is (ITERATED_LIMITS) holds

b_{1} is topological
;

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

coherence for b

( b

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

coherence for b

b

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 )

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 )

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 )

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 )

for C being Convergence-Class of T holds

( Convergence (ConvergenceSpace C) = C iff C is topological )

proof end;