:: WAYBEL17 semantic presentation

definition
let c1 be non empty set ;
let c2, c3 be Element of c1;
func c2,c3 ,... -> Function of NAT ,a1 means :Def1: :: WAYBEL17:def 1
for b1 being Nat holds
( ( ex b2 being Nat st b1 = 2 * b2 implies a4 . b1 = a2 ) & ( ( for b2 being Nat holds not b1 = 2 * b2 ) implies a4 . b1 = a3 ) );
existence
ex b1 being Function of NAT ,c1 st
for b2 being Nat holds
( ( ex b3 being Nat st b2 = 2 * b3 implies b1 . b2 = c2 ) & ( ( for b3 being Nat holds not b2 = 2 * b3 ) implies b1 . b2 = c3 ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,c1 st ( for b3 being Nat holds
( ( ex b4 being Nat st b3 = 2 * b4 implies b1 . b3 = c2 ) & ( ( for b4 being Nat holds not b3 = 2 * b4 ) implies b1 . b3 = c3 ) ) ) & ( for b3 being Nat holds
( ( ex b4 being Nat st b3 = 2 * b4 implies b2 . b3 = c2 ) & ( ( for b4 being Nat holds not b3 = 2 * b4 ) implies b2 . b3 = c3 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ,... WAYBEL17:def 1 :
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being Function of NAT ,b1 holds
( b4 = b2,b3 ,... iff for b5 being Nat holds
( ( ex b6 being Nat st b5 = 2 * b6 implies b4 . b5 = b2 ) & ( ( for b6 being Nat holds not b5 = 2 * b6 ) implies b4 . b5 = b3 ) ) );

scheme :: WAYBEL17:sch 1
s1{ F1() -> non empty TopRelStr , F2() -> non empty TopRelStr , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } :
F4() .: { F3(b1) where B is Element of F1() : P1[b1] } = { (F4() . F3(b1)) where B is Element of F1() : P1[b1] }
provided
E2: the carrier of F2() c= dom F4()
proof end;

scheme :: WAYBEL17:sch 2
s2{ F1() -> LATTICE, F2() -> LATTICE, F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } :
F4() .: { F3(b1) where B is Element of F1() : P1[b1] } = { (F4() . F3(b1)) where B is Element of F1() : P1[b1] }
provided
E2: the carrier of F2() c= dom F4()
proof end;

theorem Th1: :: WAYBEL17:1
for b1, b2 being non empty reflexive RelStr
for b3 being Function of b1,b2
for b4 being lower Subset of b2 st b3 is monotone holds
b3 " b4 is lower
proof end;

theorem Th2: :: WAYBEL17:2
for b1, b2 being non empty reflexive RelStr
for b3 being Function of b1,b2
for b4 being upper Subset of b2 st b3 is monotone holds
b3 " b4 is upper
proof end;

Lemma3: for b1 being up-complete LATTICE
for b2 being Element of b1 holds downarrow b2 is closed_under_directed_sups
proof end;

Lemma4: for b1 being up-complete Scott TopLattice
for b2 being Element of b1 holds Cl {b2} = downarrow b2
proof end;

Lemma5: for b1 being up-complete Scott TopLattice
for b2 being Element of b1 holds downarrow b2 is closed
proof end;

theorem Th3: :: WAYBEL17:3
for b1, b2 being non empty reflexive antisymmetric RelStr
for b3 being Function of b1,b2 st b3 is directed-sups-preserving holds
b3 is monotone
proof end;

registration
let c1, c2 be non empty reflexive antisymmetric RelStr ;
cluster directed-sups-preserving -> monotone Relation of the carrier of a1,the carrier of a2;
coherence
for b1 being Function of c1,c2 st b1 is directed-sups-preserving holds
b1 is monotone by Th3;
end;

theorem Th4: :: WAYBEL17:4
for b1, b2 being up-complete Scott TopLattice
for b3 being Function of b1,b2 st b3 is continuous holds
b3 is monotone
proof end;

registration
let c1, c2 be up-complete Scott TopLattice;
cluster continuous -> monotone Relation of the carrier of a1,the carrier of a2;
correctness
coherence
for b1 being Function of c1,c2 st b1 is continuous holds
b1 is monotone;
by Th4;
end;

Lemma8: for b1, b2 being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for b3 being Function of b1,b2 st b3 is directed-sups-preserving holds
b3 is continuous
proof end;

registration
let c1 be set ;
let c2 be reflexive RelStr ;
cluster K135(a1,a2) -> reflexive-yielding ;
coherence
c1 --> c2 is reflexive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be complete LATTICE;
cluster a2 |^ a1 -> complete ;
coherence
c2 |^ c1 is complete
proof end;
end;

definition
let c1, c2 be up-complete Scott TopLattice;
func SCMaps c1,c2 -> strict full SubRelStr of MonMaps a1,a2 means :Def2: :: WAYBEL17:def 2
for b1 being Function of a1,a2 holds
( b1 in the carrier of a3 iff b1 is continuous );
existence
ex b1 being strict full SubRelStr of MonMaps c1,c2 st
for b2 being Function of c1,c2 holds
( b2 in the carrier of b1 iff b2 is continuous )
proof end;
uniqueness
for b1, b2 being strict full SubRelStr of MonMaps c1,c2 st ( for b3 being Function of c1,c2 holds
( b3 in the carrier of b1 iff b3 is continuous ) ) & ( for b3 being Function of c1,c2 holds
( b3 in the carrier of b2 iff b3 is continuous ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SCMaps WAYBEL17:def 2 :
for b1, b2 being up-complete Scott TopLattice
for b3 being strict full SubRelStr of MonMaps b1,b2 holds
( b3 = SCMaps b1,b2 iff for b4 being Function of b1,b2 holds
( b4 in the carrier of b3 iff b4 is continuous ) );

registration
let c1, c2 be up-complete Scott TopLattice;
cluster SCMaps a1,a2 -> non empty strict full ;
coherence
not SCMaps c1,c2 is empty
proof end;
end;

definition
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
func Net-Str c2,c3 -> non empty strict NetStr of a1 means :Def3: :: WAYBEL17:def 3
( the carrier of a4 = NAT & the mapping of a4 = a2,a3 ,... & ( for b1, b2 being Element of a4
for b3, b4 being Nat st b1 = b3 & b2 = b4 holds
( b1 <= b2 iff b3 <= b4 ) ) );
existence
ex b1 being non empty strict NetStr of c1 st
( the carrier of b1 = NAT & the mapping of b1 = c2,c3 ,... & ( for b2, b3 being Element of b1
for b4, b5 being Nat st b2 = b4 & b3 = b5 holds
( b2 <= b3 iff b4 <= b5 ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of c1 st the carrier of b1 = NAT & the mapping of b1 = c2,c3 ,... & ( for b3, b4 being Element of b1
for b5, b6 being Nat st b3 = b5 & b4 = b6 holds
( b3 <= b4 iff b5 <= b6 ) ) & the carrier of b2 = NAT & the mapping of b2 = c2,c3 ,... & ( for b3, b4 being Element of b2
for b5, b6 being Nat st b3 = b5 & b4 = b6 holds
( b3 <= b4 iff b5 <= b6 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :
for b1 being non empty RelStr
for b2, b3 being Element of b1
for b4 being non empty strict NetStr of b1 holds
( b4 = Net-Str b2,b3 iff ( the carrier of b4 = NAT & the mapping of b4 = b2,b3 ,... & ( for b5, b6 being Element of b4
for b7, b8 being Nat st b5 = b7 & b6 = b8 holds
( b5 <= b6 iff b7 <= b8 ) ) ) );

registration
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
cluster Net-Str a2,a3 -> non empty reflexive transitive antisymmetric strict directed ;
coherence
( Net-Str c2,c3 is reflexive & Net-Str c2,c3 is transitive & Net-Str c2,c3 is directed & Net-Str c2,c3 is antisymmetric )
proof end;
end;

theorem Th5: :: WAYBEL17:5
for b1 being non empty RelStr
for b2, b3 being Element of b1
for b4 being Element of (Net-Str b2,b3) holds
( (Net-Str b2,b3) . b4 = b2 or (Net-Str b2,b3) . b4 = b3 )
proof end;

theorem Th6: :: WAYBEL17:6
for b1 being non empty RelStr
for b2, b3 being Element of b1
for b4, b5 being Element of (Net-Str b2,b3)
for b6, b7 being Nat st b6 = b4 & b7 = b6 + 1 & b7 = b5 holds
( ( (Net-Str b2,b3) . b4 = b2 implies (Net-Str b2,b3) . b5 = b3 ) & ( (Net-Str b2,b3) . b4 = b3 implies (Net-Str b2,b3) . b5 = b2 ) )
proof end;

theorem Th7: :: WAYBEL17:7
for b1 being with_infima Poset
for b2, b3 being Element of b1 holds lim_inf (Net-Str b2,b3) = b2 "/\" b3
proof end;

Lemma14: for b1 being with_infima Poset
for b2, b3 being Element of b1 st b2 <= b3 holds
lim_inf (Net-Str b2,b3) = b2
proof end;

theorem Th8: :: WAYBEL17:8
for b1, b2 being with_infima Poset
for b3, b4 being Element of b1
for b5 being Function of b1,b2 holds lim_inf (b5 * (Net-Str b3,b4)) = (b5 . b3) "/\" (b5 . b4)
proof end;

definition
let c1 be non empty RelStr ;
let c2 be non empty Subset of c1;
func Net-Str c2 -> strict NetStr of a1 equals :: WAYBEL17:def 4
 NetStr(# a2,(the InternalRel of a1 |_2 a2),((id the carrier of a1) | a2) #);
correctness
coherence
NetStr(# c2,(the InternalRel of c1 |_2 c2),((id the carrier of c1) | c2) #) is strict NetStr of c1;
;
end;

:: deftheorem Def4 defines Net-Str WAYBEL17:def 4 :
for b1 being non empty RelStr
for b2 being non empty Subset of b1 holds Net-Str b2 = NetStr(# b2,(the InternalRel of b1 |_2 b2),((id the carrier of b1) | b2) #);

theorem Th9: :: WAYBEL17:9
for b1 being non empty reflexive RelStr
for b2 being non empty Subset of b1 holds Net-Str b2 = Net-Str b2,((id the carrier of b1) | b2)
proof end;

registration
let c1 be non empty reflexive RelStr ;
let c2 be non empty directed Subset of c1;
cluster Net-Str a2 -> non empty reflexive strict directed ;
coherence
( not Net-Str c2 is empty & Net-Str c2 is directed & Net-Str c2 is reflexive )
proof end;
end;

registration
let c1 be non empty reflexive transitive RelStr ;
let c2 be non empty directed Subset of c1;
cluster Net-Str a2 -> non empty reflexive transitive strict directed ;
coherence
Net-Str c2 is transitive ;
end;

registration
let c1 be non empty reflexive RelStr ;
let c2 be non empty directed Subset of c1;
cluster Net-Str a2 -> non empty reflexive strict directed monotone ;
coherence
Net-Str c2 is monotone
proof end;
end;

Lemma17: for b1 being up-complete LATTICE
for b2 being reflexive monotone net of b1 holds lim_inf b2 = sup b2
proof end;

theorem Th10: :: WAYBEL17:10
for b1 being up-complete LATTICE
for b2 being non empty directed Subset of b1 holds lim_inf (Net-Str b2) = sup b2
proof end;

theorem Th11: :: WAYBEL17:11
for b1, b2 being LATTICE
for b3 being Function of b1,b2 st ( for b4 being net of b1 holds b3 . (lim_inf b4) <= lim_inf (b3 * b4) ) holds
b3 is monotone
proof end;

scheme :: WAYBEL17:sch 3
s3{ F1() -> non empty TopRelStr , F2() -> non empty TopRelStr , F3() -> non empty TopRelStr , F4( set ) -> Element of F3(), F5() -> Function, P1[ set ] } :
F5() .: { F4(b1) where B is Element of F1() : P1[b1] } = { (F5() . F4(b1)) where B is Element of F2() : P1[b1] }
provided
E20: the carrier of F3() c= dom F5() and
E21: the carrier of F1() = the carrier of F2()
proof end;

theorem Th12: :: WAYBEL17:12
for b1, b2 being lower-bounded continuous LATTICE
for b3 being Function of b1,b2 st b3 is directed-sups-preserving holds
for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2
proof end;

theorem Th13: :: WAYBEL17:13
for b1 being LATTICE
for b2 being lower-bounded up-complete LATTICE
for b3 being Function of b1,b2 st ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2 ) holds
b3 is monotone
proof end;

theorem Th14: :: WAYBEL17:14
for b1 being lower-bounded up-complete LATTICE
for b2 being lower-bounded continuous LATTICE
for b3 being Function of b1,b2 st ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2 ) holds
for b4 being Element of b1
for b5 being Element of b2 holds
( b5 << b3 . b4 iff ex b6 being Element of b1 st
( b6 << b4 & b5 << b3 . b6 ) )
proof end;

theorem Th15: :: WAYBEL17:15
for b1, b2 being non empty RelStr
for b3 being Subset of b1
for b4 being Function of b1,b2 st ( ( ex_sup_of b3,b1 & ex_sup_of b4 .: b3,b2 ) or ( b1 is complete & b1 is antisymmetric & b2 is complete & b2 is antisymmetric ) ) & b4 is monotone holds
sup (b4 .: b3) <= b4 . (sup b3)
proof end;

theorem Th16: :: WAYBEL17:16
for b1, b2 being non empty reflexive antisymmetric RelStr
for b3 being non empty directed Subset of b1
for b4 being Function of b1,b2 st ( ( ex_sup_of b3,b1 & ex_sup_of b4 .: b3,b2 ) or ( b1 is up-complete & b2 is up-complete ) ) & b4 is monotone holds
sup (b4 .: b3) <= b4 . (sup b3)
proof end;

theorem Th17: :: WAYBEL17:17
for b1, b2 being non empty RelStr
for b3 being Subset of b1
for b4 being Function of b1,b2 st ( ( ex_inf_of b3,b1 & ex_inf_of b4 .: b3,b2 ) or ( b1 is complete & b1 is antisymmetric & b2 is complete & b2 is antisymmetric ) ) & b4 is monotone holds
b4 . (inf b3) <= inf (b4 .: b3)
proof end;

Lemma25: for b1, b2 being complete LATTICE
for b3 being Subset of b1
for b4 being Function of b1,b2 st b4 is monotone holds
b4 . ("/\" b3,b1) <= inf (b4 .: b3)
proof end;

theorem Th18: :: WAYBEL17:18
for b1, b2 being up-complete LATTICE
for b3 being Function of b1,b2
for b4 being non empty monotone NetStr of b1 st b3 is monotone holds
b3 * b4 is monotone
proof end;

registration
let c1, c2 be up-complete LATTICE;
let c3 be monotone Function of c1,c2;
let c4 be non empty monotone NetStr of c1;
cluster a3 * a4 -> monotone ;
coherence
c3 * c4 is monotone by Th18;
end;

theorem Th19: :: WAYBEL17:19
for b1, b2 being up-complete LATTICE
for b3 being Function of b1,b2 st ( for b4 being net of b1 holds b3 . (lim_inf b4) <= lim_inf (b3 * b4) ) holds
for b4 being non empty directed Subset of b1 holds sup (b3 .: b4) = b3 . (sup b4)
proof end;

Lemma27: for b1, b2 being complete LATTICE
for b3 being Function of b1,b2 st ( for b4 being net of b1 holds b3 . (lim_inf b4) <= lim_inf (b3 * b4) ) holds
b3 is directed-sups-preserving
proof end;

theorem Th20: :: WAYBEL17:20
for b1, b2 being complete LATTICE
for b3 being Function of b1,b2
for b4 being net of b1
for b5 being Element of b4
for b6 being Element of (b3 * b4) st b6 = b5 & b3 is monotone holds
b3 . ("/\" { (b4 . b7) where B is Element of b4 : b7 >= b5 } ,b1) <= "/\" { ((b3 * b4) . b7) where B is Element of (b3 * b4) : b7 >= b6 } ,b2
proof end;

Lemma29: for b1, b2 being Scott complete TopLattice
for b3 being continuous Function of b1,b2
for b4 being net of b1 holds b3 . (lim_inf b4) <= lim_inf (b3 * b4)
proof end;

Lemma30: for b1 being continuous Scott TopLattice
for b2 being Element of b1
for b3 being Subset of b1 st b3 is open & b2 in b3 holds
ex b4 being Element of b1 st
( b4 << b2 & b4 in b3 )
proof end;

Lemma31: for b1 being lower-bounded continuous Scott TopLattice
for b2 being Element of b1 holds wayabove b2 is open
proof end;

Lemma32: for b1 being lower-bounded continuous Scott TopLattice
for b2 being Element of b1 holds { (wayabove b3) where B is Element of b1 : b3 << b2 } is Basis of b2
proof end;

Lemma33: for b1 being lower-bounded continuous Scott TopLattice holds { (wayabove b2) where B is Element of b1 : verum } is Basis of b1
proof end;

Lemma34: for b1 being lower-bounded continuous Scott TopLattice
for b2 being Subset of b1 holds Int b2 = union { (wayabove b3) where B is Element of b1 : wayabove b3 c= b2 }
proof end;

Lemma35: for b1, b2 being lower-bounded continuous Scott TopLattice
for b3 being Function of b1,b2 st ( for b4 being Element of b1
for b5 being Element of b2 holds
( b5 << b3 . b4 iff ex b6 being Element of b1 st
( b6 << b4 & b5 << b3 . b6 ) ) ) holds
b3 is continuous
proof end;

theorem Th21: :: WAYBEL17:21
for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 holds
( b3 is continuous iff for b4 being net of b1 holds b3 . (lim_inf b4) <= lim_inf (b3 * b4) )
proof end;

theorem Th22: :: WAYBEL17:22
for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 holds
( b3 is continuous iff b3 is directed-sups-preserving )
proof end;

registration
let c1, c2 be Scott complete TopLattice;
cluster continuous -> monotone directed-sups-preserving Relation of the carrier of a1,the carrier of a2;
coherence
for b1 being Function of c1,c2 st b1 is continuous holds
b1 is directed-sups-preserving by Th22;
cluster directed-sups-preserving -> continuous monotone Relation of the carrier of a1,the carrier of a2;
coherence
for b1 being Function of c1,c2 st b1 is directed-sups-preserving holds
b1 is continuous by Th22;
end;

Lemma37: for b1, b2 being continuous Scott complete TopLattice
for b3 being Function of b1,b2 st ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2 ) holds
b3 is directed-sups-preserving
proof end;

theorem Th23: :: WAYBEL17:23
for b1, b2 being continuous Scott complete TopLattice
for b3 being Function of b1,b2 holds
( b3 is continuous iff for b4 being Element of b1
for b5 being Element of b2 holds
( b5 << b3 . b4 iff ex b6 being Element of b1 st
( b6 << b4 & b5 << b3 . b6 ) ) )
proof end;

theorem Th24: :: WAYBEL17:24
for b1, b2 being continuous Scott complete TopLattice
for b3 being Function of b1,b2 holds
( b3 is continuous iff for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2 )
proof end;

Lemma40: for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st b1 is algebraic & b2 is algebraic & ( for b4 being Element of b1
for b5 being Element of b2 holds
( b5 << b3 . b4 iff ex b6 being Element of b1 st
( b6 << b4 & b5 << b3 . b6 ) ) ) holds
for b4 being Element of b1
for b5 being Element of b2 st b5 in the carrier of (CompactSublatt b2) holds
( b5 <= b3 . b4 iff ex b6 being Element of b1 st
( b6 in the carrier of (CompactSublatt b1) & b6 <= b4 & b5 <= b3 . b6 ) )
proof end;

Lemma41: for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st b1 is algebraic & b2 is algebraic & ( for b4 being Element of b1
for b5 being Element of b2 st b5 in the carrier of (CompactSublatt b2) holds
( b5 <= b3 . b4 iff ex b6 being Element of b1 st
( b6 in the carrier of (CompactSublatt b1) & b6 <= b4 & b5 <= b3 . b6 ) ) ) holds
for b4 being Element of b1
for b5 being Element of b2 holds
( b5 << b3 . b4 iff ex b6 being Element of b1 st
( b6 << b4 & b5 << b3 . b6 ) )
proof end;

Lemma42: for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st b1 is algebraic & b2 is algebraic & ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2 ) holds
for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : ( b5 <= b4 & b5 is compact ) } ,b2
proof end;

theorem Th25: :: WAYBEL17:25
for b1 being LATTICE
for b2 being complete LATTICE
for b3 being Function of b1,b2 st ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : ( b5 <= b4 & b5 is compact ) } ,b2 ) holds
b3 is monotone
proof end;

theorem Th26: :: WAYBEL17:26
for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st ( for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : ( b5 <= b4 & b5 is compact ) } ,b2 ) holds
for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : b5 << b4 } ,b2
proof end;

theorem Th27: :: WAYBEL17:27
for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st b1 is algebraic & b2 is algebraic holds
( b3 is continuous iff for b4 being Element of b1
for b5 being Element of b2 st b5 in the carrier of (CompactSublatt b2) holds
( b5 <= b3 . b4 iff ex b6 being Element of b1 st
( b6 in the carrier of (CompactSublatt b1) & b6 <= b4 & b5 <= b3 . b6 ) ) )
proof end;

theorem Th28: :: WAYBEL17:28
for b1, b2 being Scott complete TopLattice
for b3 being Function of b1,b2 st b1 is algebraic & b2 is algebraic holds
( b3 is continuous iff for b4 being Element of b1 holds b3 . b4 = "\/" { (b3 . b5) where B is Element of b1 : ( b5 <= b4 & b5 is compact ) } ,b2 )
proof end;

theorem Th29: :: WAYBEL17:29
for b1, b2 being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for b3 being Function of b1,b2 st b3 is directed-sups-preserving holds
b3 is continuous by Lemma8;