:: WAYBEL28 semantic presentation

theorem Th1: :: WAYBEL28:1

for b₁ being complete LATTICE
for b₂ being net of b₁ holds inf b₂ <= lim_inf b₂

proof end;

theorem Th2: :: WAYBEL28:2

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₁ st ( for b₄ being subnet of b₂ holds b₃ = lim_inf b₄ ) holds
( b₃ = lim_inf b₂ & ( for b₄ being subnet of b₂ holds b₃ >= inf b₄ ) )

proof end;

theorem Th3: :: WAYBEL28:3

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₁ st b₂ in NetUniv b₁ & ( for b₄ being subnet of b₂ st b₄ in NetUniv b₁ holds
b₃ = lim_inf b₄ ) holds
( b₃ = lim_inf b₂ & ( for b₄ being subnet of b₂ st b₄ in NetUniv b₁ holds
b₃ >= inf b₄ ) )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Function of c₁,c₁;
attr a₂ is greater_or_equal_to_id means :Def1: :: WAYBEL28:def 1
for b₁ being Element of a₁ holds b₁ <= a₂ . b₁;

end;

:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :

theorem Th4: :: WAYBEL28:4

for b₁ being non empty reflexive RelStr holds id b₁ is greater_or_equal_to_id

proof end;

theorem Th5: :: WAYBEL28:5

for b₁ being non empty directed RelStr
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st
( b₂ <= b₄ & b₃ <= b₄ )

proof end;

theorem Th6: :: WAYBEL28:6

for b₁ being non empty directed RelStr ex b₂ being Function of b₁,b₁ st b₂ is greater_or_equal_to_id

proof end;

registration

let c₁ be non empty directed RelStr ;
cluster greater_or_equal_to_id Relation of the carrier of a₁,the carrier of a₁;
existence by Th6;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster greater_or_equal_to_id Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
let c₃ be Function of c₂,c₂;
func c₂ * c₃ -> non empty strict NetStr of a₁ means :Def2: :: WAYBEL28:def 2
( RelStr(# the carrier of a₄,the InternalRel of a₄ #) = RelStr(# the carrier of a₂,the InternalRel of a₂ #) & the mapping of a₄ = the mapping of a₂ * a₃ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines * WAYBEL28:def 2 :

theorem Th7: :: WAYBEL28:7

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Function of b₂,b₂ holds the carrier of (b₂ * b₃) = the carrier of b₂

proof end;

theorem Th8: :: WAYBEL28:8

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Function of b₂,b₂ holds b₂ * b₃ = NetStr(# the carrier of b₂,the InternalRel of b₂,(the mapping of b₂ * b₃) #)

proof end;

theorem Th9: :: WAYBEL28:9

for b₁ being non empty 1-sorted
for b₂ being non empty transitive directed RelStr
for b₃ being Function of the carrier of b₂,the carrier of b₁ holds NetStr(# the carrier of b₂,the InternalRel of b₂,b₃ #) is net of b₁

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty transitive directed RelStr ;
let c₃ be Function of the carrier of c₂,the carrier of c₁;
cluster NetStr(# the carrier of a₂,the InternalRel of a₂,a₃ #) -> non empty transitive directed ;
correctness by Th9;

end;

theorem Th10: :: WAYBEL28:10

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Function of b₂,b₂ holds b₂ * b₃ is net of b₁

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
let c₃ be Function of c₂,c₂;
cluster a₂ * a₃ -> non empty transitive strict directed ;
correctness by Th10;

end;

theorem Th11: :: WAYBEL28:11

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Function of b₂,b₂ st b₂ in NetUniv b₁ holds
b₂ * b₃ in NetUniv b₁

proof end;

theorem Th12: :: WAYBEL28:12

for b₁ being non empty 1-sorted
for b₂, b₃ being net of b₁ st NetStr(# the carrier of b₂,the InternalRel of b₂,the mapping of b₂ #) = NetStr(# the carrier of b₃,the InternalRel of b₃,the mapping of b₃ #) holds
b₃ is subnet of b₂

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
cluster strict subnet of a₂;
existence

proof end;

end;

theorem Th13: :: WAYBEL28:13

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being greater_or_equal_to_id Function of b₂,b₂ holds b₂ * b₃ is subnet of b₂

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
let c₃ be greater_or_equal_to_id Function of c₂,c₂;
redefine func * as c₂ * c₃ -> strict subnet of a₂;
correctness by Th13;

end;

theorem Th14: :: WAYBEL28:14

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₁ st b₂ in NetUniv b₁ & b₃ = lim_inf b₂ & ( for b₄ being subnet of b₂ st b₄ in NetUniv b₁ holds
b₃ >= inf b₄ ) holds
( b₃ = lim_inf b₂ & ( for b₄ being greater_or_equal_to_id Function of b₂,b₂ holds b₃ >= inf (b₂ * b₄) ) )

proof end;

theorem Th15: :: WAYBEL28:15

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₁ st b₃ = lim_inf b₂ & ( for b₄ being greater_or_equal_to_id Function of b₂,b₂ holds b₃ >= inf (b₂ * b₄) ) holds
for b₄ being subnet of b₂ holds b₃ = lim_inf b₄

proof end;

definition

let c₁ be non empty RelStr ;
func lim_inf-Convergence c₁ -> Convergence-Class of a₁ means :Def3: :: WAYBEL28:def 3
for b₁ being net of a₁ st b₁ in NetUniv a₁ holds
for b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff for b₃ being subnet of b₁ holds b₂ = lim_inf b₃ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th16: :: WAYBEL28:16

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Element of b₁ st b₂ in NetUniv b₁ holds
( [b₂,b₃] in lim_inf-Convergence b₁ iff for b₄ being subnet of b₂ st b₄ in NetUniv b₁ holds
b₃ = lim_inf b₄ )

proof end;

theorem Th17: :: WAYBEL28:17

for b₁ being non empty RelStr
for b₂ being constant net of b₁
for b₃ being subnet of b₂ holds
( b₃ is constant & the_value_of b₂ = the_value_of b₃ )

proof end;

definition

let c₁ be non empty RelStr ;
func xi c₁ -> Subset-Family of a₁ equals :: WAYBEL28:def 4
the topology of (ConvergenceSpace (lim_inf-Convergence a₁));
correctness by YELLOW_6:def 27;

end;

:: deftheorem Def4 defines xi WAYBEL28:def 4 :

theorem Th18: :: WAYBEL28:18

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

proof end;

theorem Th19: :: WAYBEL28:19

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

proof end;

theorem Th20: :: WAYBEL28:20

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

proof end;

theorem Th21: :: WAYBEL28:21

for b₁ being non empty RelStr
for b₂, b₃ being set st [b₂,b₃] in lim_inf-Convergence b₁ holds
b₂ in NetUniv b₁

proof end;

theorem Th22: :: WAYBEL28:22

for b₁ being non empty 1-sorted
for b₂, b₃ being Convergence-Class of b₁ st b₂ c= b₃ holds
the topology of (ConvergenceSpace b₃) c= the topology of (ConvergenceSpace b₂)

proof end;

theorem Th23: :: WAYBEL28:23

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

proof end;

theorem Th24: :: WAYBEL28:24

for b₁, b₂ being set st b₁ c= b₂ holds
b₁ in the_universe_of b₂

proof end;

theorem Th25: :: WAYBEL28:25

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty directed Subset of b₁ holds Net-Str b₂ in NetUniv b₁

proof end;

theorem Th26: :: WAYBEL28:26

for b₁ being complete LATTICE
for b₂ being non empty directed Subset of b₁
for b₃ being subnet of Net-Str b₂ holds lim_inf b₃ = sup b₂

proof end;

theorem Th27: :: WAYBEL28:27

for b₁ being non empty complete LATTICE
for b₂ being non empty directed Subset of b₁ holds [(Net-Str b₂),(sup b₂)] in lim_inf-Convergence b₁

proof end;

theorem Th28: :: WAYBEL28:28

for b₁ being complete LATTICE
for b₂ being Subset of b₁ st b₂ in xi b₁ holds
b₂ is property(S)

proof end;

theorem Th29: :: WAYBEL28:29

for b₁ being non empty reflexive RelStr
for b₂ being Subset of b₁ st b₂ in sigma b₁ holds
b₂ in xi b₁

proof end;

theorem Th30: :: WAYBEL28:30

for b₁ being complete LATTICE
for b₂ being Subset of b₁ st b₂ is upper & b₂ in xi b₁ holds
b₂ in sigma b₁

proof end;

theorem Th31: :: WAYBEL28:31

for b₁ being complete LATTICE
for b₂ being Subset of b₁ st b₂ is lower holds
( b₂ ` in xi b₁ iff b₂ is closed_under_directed_sups )

proof end;