:: by Bart{\l}omiej Skorulski

::

:: Received January 6, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

theorem :: WAYBEL28:2

for L being complete LATTICE

for N being net of L

for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

for N being net of L

for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

proof end;

theorem Th3: :: WAYBEL28:3

for L being complete LATTICE

for N being net of L

for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

for N being net of L

for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

proof end;

definition

let N be non empty RelStr ;

let f be Function of N,N;

end;
let f be Function of N,N;

attr f is greater_or_equal_to_id means :Def1: :: WAYBEL28:def 1

for j being Element of N holds j <= f . j;

for j being Element of N holds j <= f . j;

:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :

for N being non empty RelStr

for f being Function of N,N holds

( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j );

for N being non empty RelStr

for f being Function of N,N holds

( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j );

theorem Th5: :: WAYBEL28:5

for N being non empty directed RelStr

for x, y being Element of N ex z being Element of N st

( x <= z & y <= z )

for x, y being Element of N ex z being Element of N st

( x <= z & y <= z )

proof end;

registration

let N be non empty directed RelStr ;

ex b_{1} being Function of N,N st b_{1} is greater_or_equal_to_id

end;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];

existence ex b

proof end;

registration

let N be non empty reflexive RelStr ;

ex b_{1} being Function of N,N st b_{1} is greater_or_equal_to_id

end;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];

existence ex b

proof end;

definition

let L be non empty 1-sorted ;

let N be non empty NetStr over L;

let f be Function of N,N;

ex b_{1} being non empty strict NetStr over L st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = the mapping of N * f )

for b_{1}, b_{2} being non empty strict NetStr over L st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{1} = the mapping of N * f & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{2} = the mapping of N * f holds

b_{1} = b_{2}
;

end;
let N be non empty NetStr over L;

let f be Function of N,N;

func N * f -> non empty strict NetStr over L means :Def2: :: WAYBEL28:def 2

( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = the mapping of N * f );

existence ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = the mapping of N * f );

ex b

( RelStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines * WAYBEL28:def 2 :

for L being non empty 1-sorted

for N being non empty NetStr over L

for f being Function of N,N

for b_{4} being non empty strict NetStr over L holds

( b_{4} = N * f iff ( RelStr(# the carrier of b_{4}, the InternalRel of b_{4} #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b_{4} = the mapping of N * f ) );

for L being non empty 1-sorted

for N being non empty NetStr over L

for f being Function of N,N

for b

( b

theorem Th6: :: WAYBEL28:6

for L being non empty 1-sorted

for N being non empty NetStr over L

for f being Function of N,N holds the carrier of (N * f) = the carrier of N

for N being non empty NetStr over L

for f being Function of N,N holds the carrier of (N * f) = the carrier of N

proof end;

theorem Th7: :: WAYBEL28:7

for L being non empty 1-sorted

for N being non empty NetStr over L

for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)

for N being non empty NetStr over L

for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)

proof end;

theorem Th8: :: WAYBEL28:8

for L being non empty 1-sorted

for N being non empty transitive directed RelStr

for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L

for N being non empty transitive directed RelStr

for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L

proof end;

registration

let L be non empty 1-sorted ;

let N be non empty transitive directed RelStr ;

let f be Function of the carrier of N, the carrier of L;

correctness

coherence

( NetStr(# the carrier of N, the InternalRel of N,f #) is transitive & NetStr(# the carrier of N, the InternalRel of N,f #) is directed & not NetStr(# the carrier of N, the InternalRel of N,f #) is empty );

by Th8;

end;
let N be non empty transitive directed RelStr ;

let f be Function of the carrier of N, the carrier of L;

correctness

coherence

( NetStr(# the carrier of N, the InternalRel of N,f #) is transitive & NetStr(# the carrier of N, the InternalRel of N,f #) is directed & not NetStr(# the carrier of N, the InternalRel of N,f #) is empty );

by Th8;

theorem Th9: :: WAYBEL28:9

for L being non empty 1-sorted

for N being net of L

for p being Function of N,N holds N * p is net of L

for N being net of L

for p being Function of N,N holds N * p is net of L

proof end;

registration

let L be non empty 1-sorted ;

let N be net of L;

let p be Function of N,N;

correctness

coherence

( N * p is transitive & N * p is directed );

by Th9;

end;
let N be net of L;

let p be Function of N,N;

correctness

coherence

( N * p is transitive & N * p is directed );

by Th9;

theorem Th10: :: WAYBEL28:10

for L being non empty 1-sorted

for N being net of L

for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

for N being net of L

for p being Function of N,N st N in NetUniv L holds

N * p in NetUniv L

proof end;

theorem :: WAYBEL28:11

for L being non empty 1-sorted

for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds

M is subnet of N

for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds

M is subnet of N

proof end;

theorem Th12: :: WAYBEL28:12

for L being non empty 1-sorted

for N being net of L

for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N

for N being net of L

for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N

proof end;

definition

let L be non empty 1-sorted ;

let N be net of L;

let p be greater_or_equal_to_id Function of N,N;

:: original: *

redefine func N * p -> strict subnet of N;

correctness

coherence

N * p is strict subnet of N;

by Th12;

end;
let N be net of L;

let p be greater_or_equal_to_id Function of N,N;

:: original: *

redefine func N * p -> strict subnet of N;

correctness

coherence

N * p is strict subnet of N;

by Th12;

theorem :: WAYBEL28:13

theorem Th14: :: WAYBEL28:14

for L being complete LATTICE

for N being net of L

for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds

for M being subnet of N holds x = lim_inf M

for N being net of L

for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds

for M being subnet of N holds x = lim_inf M

proof end;

definition

let L be non empty RelStr ;

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

for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in b_{1} iff for M being subnet of N holds x = lim_inf M )

for b_{1}, b_{2} being Convergence-Class of L st ( for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in b_{1} iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in b_{2} iff for M being subnet of N holds x = lim_inf M ) ) holds

b_{1} = b_{2}

end;
func lim_inf-Convergence L -> Convergence-Class of L means :Def3: :: WAYBEL28:def 3

for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in it iff for M being subnet of N holds x = lim_inf M );

existence for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in it iff for M being subnet of N holds x = lim_inf M );

ex b

for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in b

proof end;

uniqueness for b

for x being Element of L holds

( [N,x] in b

for x being Element of L holds

( [N,x] in b

b

proof end;

:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def 3 :

for L being non empty RelStr

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

( b_{2} = lim_inf-Convergence L iff for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in b_{2} iff for M being subnet of N holds x = lim_inf M ) );

for L being non empty RelStr

for b

( b

for x being Element of L holds

( [N,x] in b

theorem :: WAYBEL28:15

for L being complete LATTICE

for N being net of L

for x being Element of L st N in NetUniv L holds

( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds

x = lim_inf M )

for N being net of L

for x being Element of L st N in NetUniv L holds

( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds

x = lim_inf M )

proof end;

theorem Th16: :: WAYBEL28:16

for L being non empty RelStr

for N being constant net of L

for M being subnet of N holds

( M is constant & the_value_of N = the_value_of M )

for N being constant net of L

for M being subnet of N holds

( M is constant & the_value_of N = the_value_of M )

proof end;

definition

let L be non empty RelStr ;

coherence

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Subset-Family of L;

by YELLOW_6:def 24;

end;
func xi L -> Subset-Family of L equals :: WAYBEL28:def 4

the topology of (ConvergenceSpace (lim_inf-Convergence L));

correctness the topology of (ConvergenceSpace (lim_inf-Convergence L));

coherence

the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Subset-Family of L;

by YELLOW_6:def 24;

:: deftheorem defines xi WAYBEL28:def 4 :

for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L));

for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L));

theorem :: WAYBEL28:20

for L being non empty RelStr

for N, x being set st [N,x] in lim_inf-Convergence L holds

N in NetUniv L

for N, x being set st [N,x] in lim_inf-Convergence L holds

N in NetUniv L

proof end;

theorem Th21: :: WAYBEL28:21

for L being non empty 1-sorted

for C1, C2 being Convergence-Class of L st C1 c= C2 holds

the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

for C1, C2 being Convergence-Class of L st C1 c= C2 holds

the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

proof end;

theorem Th24: :: WAYBEL28:24

for L being non empty reflexive transitive RelStr

for D being non empty directed Subset of L holds Net-Str D in NetUniv L

for D being non empty directed Subset of L holds Net-Str D in NetUniv L

proof end;

theorem Th25: :: WAYBEL28:25

for L being complete LATTICE

for D being non empty directed Subset of L

for M being subnet of Net-Str D holds lim_inf M = sup D

for D being non empty directed Subset of L

for M being subnet of Net-Str D holds lim_inf M = sup D

proof end;

theorem Th26: :: WAYBEL28:26

for L being non empty complete LATTICE

for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L

for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L

proof end;

theorem :: WAYBEL28:30

for L being complete LATTICE

for A being Subset of L st A is lower holds

( A ` in xi L iff A is closed_under_directed_sups )

for A being Subset of L st A is lower holds

( A ` in xi L iff A is closed_under_directed_sups )

proof end;