WAYBEL28: Lim-inf Convergence

:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: WAYBEL28:1

for L being complete LATTICE
for N being net of L holds inf N <= lim_inf N

proof end;

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

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

proof end;

definition

let N be non empty RelStr ;
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;

end;

:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :

theorem Th4: :: WAYBEL28:4

for N being non empty reflexive RelStr holds id N is greater_or_equal_to_id

proof end;

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 )

proof end;

registration

let N be non empty directed RelStr ;

cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V37( the carrier of N) V38( 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

proof end;

end;

registration

let N be non empty reflexive RelStr ;

existence

proof end;

end;

definition

let L be non empty 1-sorted ;
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

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines * WAYBEL28:def 2 :

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

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

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

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;

cluster NetStr(# the carrier of N, the InternalRel of N,f #) -> non empty transitive directed ;

correctness by Th8;

end;

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

proof end;

registration

let L be non empty 1-sorted ;
let N be net of L;
let p be Function of N,N;

cluster N * p -> non empty transitive strict directed ;

correctness by Th9;

end;

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

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

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

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

end;

theorem :: WAYBEL28:13

for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L & x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) holds
( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) ) by Th10;

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

proof end;

definition

let L be non empty RelStr ;

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

proof end;

uniqueness

proof end;

end;

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

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 )

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 )

proof end;

definition

let L be non empty RelStr ;

func xi L -> Subset-Family of L equals :: WAYBEL28:def 4
the topology of (ConvergenceSpace (lim_inf-Convergence L));

correctness by YELLOW_6:def 24;

end;

:: deftheorem defines xi WAYBEL28:def 4 :

theorem :: WAYBEL28:17

for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)

proof end;

theorem :: WAYBEL28:18

for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)

proof end;

theorem :: WAYBEL28:19

for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE)

proof end;

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

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)

proof end;

theorem Th22: :: WAYBEL28:22

for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L

proof end;

theorem Th23: :: WAYBEL28:23

for X, Y being set st X c= Y holds
X in the_universe_of Y

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

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

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

proof end;

theorem Th27: :: WAYBEL28:27

for L being complete LATTICE
for U1 being Subset of L st U1 in xi L holds
U1 is property(S)

proof end;

theorem Th28: :: WAYBEL28:28

for L being non empty reflexive RelStr
for A being Subset of L st A in sigma L holds
A in xi L

proof end;

theorem Th29: :: WAYBEL28:29

for L being complete LATTICE
for A being Subset of L st A is upper & A in xi L holds
A in sigma 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 )

proof end;