:: WAYBEL17 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let S be non empty set ;
let a, b be Element of S;
func a,b ,... -> Function of NAT ,S means :Def1: :: WAYBEL17:def 1
for i being Nat holds
( ( ex k being Nat st i = 2 * k implies it . i = a ) & ( ( for k being Nat holds not i = 2 * k ) implies it . i = b ) );
existence
ex b1 being Function of NAT ,S st
for i being Nat holds
( ( ex k being Nat st i = 2 * k implies b1 . i = a ) & ( ( for k being Nat holds not i = 2 * k ) implies b1 . i = b ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,S st ( for i being Nat holds
( ( ex k being Nat st i = 2 * k implies b1 . i = a ) & ( ( for k being Nat holds not i = 2 * k ) implies b1 . i = b ) ) ) & ( for i being Nat holds
( ( ex k being Nat st i = 2 * k implies b2 . i = a ) & ( ( for k being Nat holds not i = 2 * k ) implies b2 . i = b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ,... WAYBEL17:def 1 :
for S being non empty set
for a, b being Element of S
for b4 being Function of NAT ,S holds
( b4 = a,b ,... iff for i being Nat holds
( ( ex k being Nat st i = 2 * k implies b4 . i = a ) & ( ( for k being Nat holds not i = 2 * k ) implies b4 . i = b ) ) );

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

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

theorem Th1: :: WAYBEL17:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty reflexive RelStr
for f being Function of S,T
for P being lower Subset of T st f is monotone holds
f " P is lower
proof end;

theorem :: WAYBEL17:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty reflexive RelStr
for f being Function of S,T
for P being upper Subset of T st f is monotone holds
f " P is upper
proof end;

Lm1: for T being up-complete LATTICE
for x being Element of T holds downarrow x is closed_under_directed_sups
proof end;

Lm2: for T being up-complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proof end;

Lm3: for T being up-complete Scott TopLattice
for x being Element of T holds downarrow x is closed
proof end;

theorem Th3: :: WAYBEL17:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty reflexive antisymmetric RelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
proof end;

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

theorem Th4: :: WAYBEL17:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being up-complete Scott TopLattice
for f being Function of S,T st f is continuous holds
f is monotone
proof end;

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

Lm4: for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is continuous
proof end;

registration
let S be set ;
let T be reflexive RelStr ;
cluster K135(S,T) -> reflexive-yielding ;
coherence
S --> T is reflexive-yielding
proof end;
end;

registration
let S be non empty set ;
let T be complete LATTICE;
cluster T |^ S -> complete ;
coherence
T |^ S is complete
proof end;
end;

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

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

registration
let S, T be up-complete Scott TopLattice;
cluster SCMaps S,T -> non empty strict full ;
coherence
not SCMaps S,T is empty
proof end;
end;

definition
let S be non empty RelStr ;
let a, b be Element of S;
func Net-Str a,b -> non empty strict NetStr of S means :Def3: :: WAYBEL17:def 3
( the carrier of it = NAT & the mapping of it = a,b ,... & ( for i, j being Element of it
for i', j' being Nat st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) );
existence
ex b1 being non empty strict NetStr of S st
( the carrier of b1 = NAT & the mapping of b1 = a,b ,... & ( for i, j being Element of b1
for i', j' being Nat st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of S st the carrier of b1 = NAT & the mapping of b1 = a,b ,... & ( for i, j being Element of b1
for i', j' being Nat st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) & the carrier of b2 = NAT & the mapping of b2 = a,b ,... & ( for i, j being Element of b2
for i', j' being Nat st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :
for S being non empty RelStr
for a, b being Element of S
for b4 being non empty strict NetStr of S holds
( b4 = Net-Str a,b iff ( the carrier of b4 = NAT & the mapping of b4 = a,b ,... & ( for i, j being Element of b4
for i', j' being Nat st i = i' & j = j' holds
( i <= j iff i' <= j' ) ) ) );

registration
let S be non empty RelStr ;
let a, b be Element of S;
cluster Net-Str a,b -> non empty reflexive transitive antisymmetric strict directed ;
coherence
( Net-Str a,b is reflexive & Net-Str a,b is transitive & Net-Str a,b is directed & Net-Str a,b is antisymmetric )
proof end;
end;

theorem Th5: :: WAYBEL17:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty RelStr
for a, b being Element of S
for i being Element of (Net-Str a,b) holds
( (Net-Str a,b) . i = a or (Net-Str a,b) . i = b )
proof end;

theorem Th6: :: WAYBEL17:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty RelStr
for a, b being Element of S
for i, j being Element of (Net-Str a,b)
for i', j' being Nat st i' = i & j' = i' + 1 & j' = j holds
( ( (Net-Str a,b) . i = a implies (Net-Str a,b) . j = b ) & ( (Net-Str a,b) . i = b implies (Net-Str a,b) . j = a ) )
proof end;

theorem Th7: :: WAYBEL17:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being with_infima Poset
for a, b being Element of S holds lim_inf (Net-Str a,b) = a "/\" b
proof end;

Lm5: for S being with_infima Poset
for a, b being Element of S st a <= b holds
lim_inf (Net-Str a,b) = a
proof end;

theorem Th8: :: WAYBEL17:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being with_infima Poset
for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str a,b)) = (f . a) "/\" (f . b)
proof end;

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

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

theorem Th9: :: WAYBEL17:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty reflexive RelStr
for D being non empty Subset of S holds Net-Str D = Net-Str D,((id the carrier of S) | D)
proof end;

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

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

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

Lm6: for R being up-complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proof end;

theorem Th10: :: WAYBEL17:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being up-complete LATTICE
for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D
proof end;

theorem Th11: :: WAYBEL17:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is monotone
proof end;

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

theorem Th12: :: WAYBEL17:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being lower-bounded continuous LATTICE
for f being Function of S,T st f is directed-sups-preserving holds
for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T
proof end;

theorem Th13: :: WAYBEL17:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being LATTICE
for T being lower-bounded up-complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
f is monotone
proof end;

theorem Th14: :: WAYBEL17:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being lower-bounded up-complete LATTICE
for T being lower-bounded continuous LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
proof end;

theorem Th15: :: WAYBEL17:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for D being Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
proof end;

theorem Th16: :: WAYBEL17:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty reflexive antisymmetric RelStr
for D being non empty directed Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
proof end;

theorem :: WAYBEL17:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty RelStr
for D being Subset of S
for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
f . (inf D) <= inf (f .: D)
proof end;

Lm7: for S, T being complete LATTICE
for D being Subset of S
for f being Function of S,T st f is monotone holds
f . ("/\" D,S) <= inf (f .: D)
proof end;

theorem Th18: :: WAYBEL17:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being up-complete LATTICE
for f being Function of S,T
for N being non empty monotone NetStr of S st f is monotone holds
f * N is monotone
proof end;

registration
let S, T be up-complete LATTICE;
let f be monotone Function of S,T;
let N be non empty monotone NetStr of S;
cluster f * N -> monotone ;
coherence
f * N is monotone
by Th18;
end;

theorem :: WAYBEL17:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being up-complete LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
proof end;

Lm8: for S, T being complete LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is directed-sups-preserving
proof end;

theorem Th20: :: WAYBEL17:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being complete LATTICE
for f being Function of S,T
for N being net of S
for j being Element of N
for j' being Element of (f * N) st j' = j & f is monotone holds
f . ("/\" { (N . k) where k is Element of N : k >= j } ,S) <= "/\" { ((f * N) . l) where l is Element of (f * N) : l >= j' } ,T
proof end;

Lm9: for S, T being Scott complete TopLattice
for f being continuous Function of S,T
for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
proof end;

Lm10: for L being continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
proof end;

Lm11: for L being lower-bounded continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proof end;

Lm12: for L being lower-bounded continuous Scott TopLattice
for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of p
proof end;

Lm13: for T being lower-bounded continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T
proof end;

Lm14: for T being lower-bounded continuous Scott TopLattice
for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
proof end;

Lm15: for S, T being lower-bounded continuous Scott TopLattice
for f being Function of S,T st ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
f is continuous
proof end;

theorem :: WAYBEL17:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Scott complete TopLattice
for f being Function of S,T holds
( f is continuous iff for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) )
proof end;

theorem Th22: :: WAYBEL17:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Scott complete TopLattice
for f being Function of S,T holds
( f is continuous iff f is directed-sups-preserving )
proof end;

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

Lm16: for S, T being continuous Scott complete TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
f is directed-sups-preserving
proof end;

theorem Th23: :: WAYBEL17:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being continuous Scott complete TopLattice
for f being Function of S,T holds
( f is continuous iff for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
proof end;

theorem Th24: :: WAYBEL17:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being continuous Scott complete TopLattice
for f being Function of S,T holds
( f is continuous iff for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T )
proof end;

Lm17: for S, T being Scott complete TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
proof end;

Lm18: for S, T being Scott complete TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
proof end;

Lm19: for S, T being Scott complete TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T
proof end;

theorem Th25: :: WAYBEL17:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being LATTICE
for T being complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ) holds
f is monotone
proof end;

theorem Th26: :: WAYBEL17:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Scott complete TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T ) holds
for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T
proof end;

theorem :: WAYBEL17:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Scott complete TopLattice
for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
proof end;

theorem :: WAYBEL17:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Scott complete TopLattice
for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T )
proof end;

theorem :: WAYBEL17:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is continuous by Lm4;