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

theorem :: WAYBEL24: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 up-complete Scott TopLattice
for M being Subset of (SCMaps S,T) holds "\/" M,(SCMaps S,T) is continuous Function of S,T
proof end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster constant -> monotone M4(the carrier of S,the carrier of T);
coherence
for b1 being Function of S,T st b1 is constant holds
b1 is monotone
proof end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
let a be Element of T;
cluster S --> a -> monotone ;
coherence
S --> a is monotone
proof end;
end;

theorem :: WAYBEL24:2  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 T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps S,T) = S --> (Bottom T)
proof end;

theorem :: WAYBEL24:3  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 T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps S,T) = S --> (Top T)
proof end;

scheme :: WAYBEL24:sch 1
FuncFraenkelSL{ F1() -> non empty RelStr , F2() -> non empty RelStr , 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 :: WAYBEL24:sch 2
Fraenkel6A{ F1() -> LATTICE, F2( set ) -> set , P1[ set ], P2[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] }
provided
A1: for v being Element of F1() holds
( P1[v] iff P2[v] )
proof end;

theorem Th4: :: WAYBEL24: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 complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
proof end;

theorem :: WAYBEL24:5  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 complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w <= x } ,T
proof end;

theorem Th6: :: WAYBEL24:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RelStr
for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
proof end;

definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let x be Element of X1;
func Proj f,x -> Function of X2,Y equals :: WAYBEL24:def 1
(curry f) . x;
correctness
coherence
(curry f) . x is Function of X2,Y
;
proof end;
end;

:: deftheorem defines Proj WAYBEL24:def 1 :
for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1 holds Proj f,x = (curry f) . x;

theorem Th7: :: WAYBEL24:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X1, X2 being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj f,x) . y = f . [x,y]
proof end;

definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let y be Element of X2;
func Proj f,y -> Function of X1,Y equals :: WAYBEL24:def 2
(curry' f) . y;
correctness
coherence
(curry' f) . y is Function of X1,Y
;
proof end;
end;

:: deftheorem defines Proj WAYBEL24:def 2 :
for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2 holds Proj f,y = (curry' f) . y;

theorem Th8: :: WAYBEL24:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X2, X1 being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj f,y) . x = f . [x,y]
proof end;

theorem Th9: :: WAYBEL24:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being non empty RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj f,a) . b = (Proj f,b) . a
proof end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster antitone M4(the carrier of S,the carrier of T);
existence
ex b1 being Function of S,T st b1 is antitone
proof end;
end;

theorem Th10: :: WAYBEL24:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj f,a is monotone & Proj f,b is monotone )
proof end;

theorem Th11: :: WAYBEL24:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is antitone holds
( Proj f,a is antitone & Proj f,b is antitone )
proof end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let a be Element of R;
cluster Proj f,a -> monotone ;
coherence
Proj f,a is monotone
by Th10;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let b be Element of S;
cluster Proj f,b -> monotone ;
coherence
Proj f,b is monotone
by Th10;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let a be Element of R;
cluster Proj f,a -> antitone ;
coherence
Proj f,a is antitone
by Th11;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let b be Element of S;
cluster Proj f,b -> antitone ;
coherence
Proj f,b is antitone
by Th11;
end;

theorem Th12: :: WAYBEL24:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj f,a is monotone & Proj f,b is monotone ) ) holds
f is monotone
proof end;

theorem :: WAYBEL24:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj f,a is antitone & Proj f,b is antitone ) ) holds
f is antitone
proof end;

theorem Th14: :: WAYBEL24:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj f,b) .: X = f .: [:X,{b}:]
proof end;

theorem Th15: :: WAYBEL24:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj f,b) .: X = f .: [:{b},X:]
proof end;

theorem :: WAYBEL24:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj f,a is directed-sups-preserving & Proj f,b is directed-sups-preserving )
proof end;

theorem Th17: :: WAYBEL24:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being LATTICE
for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
proof end;

theorem :: WAYBEL24:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being complete LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj f,a is directed-sups-preserving & Proj f,b is directed-sups-preserving ) ) holds
f is directed-sups-preserving
proof end;

theorem Th19: :: WAYBEL24:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being set
for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S,the carrier of T )
proof end;

definition
let S be TopStruct ;
let T be non empty TopRelStr ;
func ContMaps S,T -> strict RelStr means :Def3: :: WAYBEL24:def 3
( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of it iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) );
existence
ex b1 being strict RelStr st
( b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
proof end;
uniqueness
for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :
for S being TopStruct
for T being non empty TopRelStr
for b3 being strict RelStr holds
( b3 = ContMaps S,T iff ( b3 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b3 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) ) );

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps S,T -> non empty strict ;
coherence
not ContMaps S,T is empty
proof end;
end;

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps S,T -> non empty strict constituted-Functions ;
coherence
ContMaps S,T is constituted-Functions
proof end;
end;

theorem Th20: :: WAYBEL24:20  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 TopSpace
for T being non empty reflexive TopSpace-like TopRelStr
for x, y being Element of (ContMaps S,T) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
proof end;

theorem Th21: :: WAYBEL24:21  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 TopSpace
for T being non empty reflexive TopSpace-like TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps S,T) )
proof end;

registration
let S be non empty TopSpace;
let T be non empty reflexive TopSpace-like TopRelStr ;
cluster ContMaps S,T -> non empty strict reflexive constituted-Functions ;
coherence
ContMaps S,T is reflexive
proof end;
end;

registration
let S be non empty TopSpace;
let T be non empty transitive TopSpace-like TopRelStr ;
cluster ContMaps S,T -> non empty strict transitive constituted-Functions ;
coherence
ContMaps S,T is transitive
proof end;
end;

registration
let S be non empty TopSpace;
let T be non empty antisymmetric TopSpace-like TopRelStr ;
cluster ContMaps S,T -> non empty strict antisymmetric constituted-Functions ;
coherence
ContMaps S,T is antisymmetric
proof end;
end;

registration
let S be set ;
let T be non empty RelStr ;
cluster T |^ S -> constituted-Functions ;
coherence
T |^ S is constituted-Functions
proof end;
end;

theorem :: WAYBEL24:22  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 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" {f,g},(T |^ the carrier of S) holds
h . i = sup {(f . i),(g . i)}
proof end;

theorem Th23: :: WAYBEL24:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi X,i)
proof end;

theorem :: WAYBEL24:24  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 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" {f,g},(T |^ the carrier of S) holds
h . i = inf {(f . i),(g . i)}
proof end;

theorem Th25: :: WAYBEL24:25  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 T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T
proof end;

theorem Th26: :: WAYBEL24: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 complete TopLattice
for F being non empty Subset of (ContMaps S,T)
for i being Element of S holds ("\/" F,(T |^ the carrier of S)) . i = "\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T
proof end;

theorem Th27: :: WAYBEL24:27  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 T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
proof end;

theorem Th28: :: WAYBEL24: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 non empty Subset of (ContMaps S,T)
for D being non empty Subset of S holds ("\/" F,(T |^ the carrier of S)) .: D = { ("\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) where i is Element of S : i in D }
proof end;

scheme :: WAYBEL24:sch 3
FraenkelF'RS{ F1() -> non empty TopRelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof end;

scheme :: WAYBEL24:sch 4
FraenkelF'RSS{ F1() -> non empty RelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof end;

scheme :: WAYBEL24:sch 5
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;

Lm1: for S being non empty RelStr
for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
proof end;

theorem Th29: :: WAYBEL24: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 Scott complete TopLattice
for F being non empty Subset of (ContMaps S,T) holds "\/" F,(T |^ the carrier of S) is monotone Function of S,T
proof end;

theorem Th30: :: WAYBEL24:30  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 non empty Subset of (ContMaps S,T)
for D being non empty directed Subset of S holds "\/" { ("\/" { (g . i) where i is Element of S : i in D } ,T) where g is Element of (T |^ the carrier of S) : g in F } ,T = "\/" { ("\/" { (g' . i') where g' is Element of (T |^ the carrier of S) : g' in F } ,T) where i' is Element of S : i' in D } ,T
proof end;

theorem Th31: :: WAYBEL24:31  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 non empty Subset of (ContMaps S,T)
for D being non empty directed Subset of S holds "\/" (("\/" F,(T |^ the carrier of S)) .: D),T = ("\/" F,(T |^ the carrier of S)) . (sup D)
proof end;

theorem Th32: :: WAYBEL24:32  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 non empty Subset of (ContMaps S,T) holds "\/" F,(T |^ the carrier of S) in the carrier of (ContMaps S,T)
proof end;

theorem Th33: :: WAYBEL24:33  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 T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
proof end;

theorem :: WAYBEL24:34  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 T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)
proof end;

registration
let S be non empty reflexive RelStr ;
let T be complete LATTICE;
let a be Element of T;
cluster S --> a -> monotone directed-sups-preserving ;
coherence
S --> a is directed-sups-preserving
proof end;
end;

theorem Th35: :: WAYBEL24:35  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 holds ContMaps S,T is sups-inheriting SubRelStr of T |^ the carrier of S
proof end;

registration
let S, T be Scott complete TopLattice;
cluster ContMaps S,T -> non empty strict reflexive transitive antisymmetric complete constituted-Functions ;
coherence
ContMaps S,T is complete
proof end;
end;

theorem :: WAYBEL24:36  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 Scott complete TopLattice holds Bottom (ContMaps S,T) = S --> (Bottom T)
proof end;

theorem :: WAYBEL24:37  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 Scott complete TopLattice holds Top (ContMaps S,T) = S --> (Top T)
proof end;

theorem :: WAYBEL24:38  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 holds SCMaps S,T = ContMaps S,T
proof end;