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

notation
let I be set ;
let J be RelStr-yielding ManySortedSet of I;
synonym I -POS_prod J for product J;
end;

registration
let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster I -POS_prod J -> constituted-Functions ;
coherence
I -POS_prod J is constituted-Functions
;
end;

notation
let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
synonym I -TOP_prod J for product J;
end;

definition
let X, Y be non empty TopSpace;
func oContMaps X,Y -> non empty strict RelStr equals :: WAYBEL26:def 1
ContMaps X,(Omega Y);
coherence
ContMaps X,(Omega Y) is non empty strict RelStr
;
end;

:: deftheorem defines oContMaps WAYBEL26:def 1 :
for X, Y being non empty TopSpace holds oContMaps X,Y = ContMaps X,(Omega Y);

registration
let X, Y be non empty TopSpace;
cluster oContMaps X,Y -> non empty strict reflexive transitive constituted-Functions ;
coherence
( oContMaps X,Y is reflexive & oContMaps X,Y is transitive & oContMaps X,Y is constituted-Functions )
;
end;

registration
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps X,Y -> non empty strict reflexive transitive antisymmetric constituted-Functions ;
coherence
oContMaps X,Y is antisymmetric
;
end;

theorem Th1: :: WAYBEL26:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps X,Y) iff a is continuous Function of X,(Omega Y) )
proof end;

theorem Th2: :: WAYBEL26:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps X,Y) iff a is continuous Function of X,Y )
proof end;

theorem Th3: :: WAYBEL26:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for a, b being Element of (oContMaps X,Y)
for f, g being Function of X,(Omega Y) st a = f & b = g holds
( a <= b iff f <= g )
proof end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let A be Subset of (oContMaps X,Y);
:: original: pi
redefine func pi A,x -> Subset of (Omega Y);
coherence
pi A,x is Subset of (Omega Y)
proof end;
end;

registration
let X, Y be non empty TopSpace;
let x be set ;
let A be non empty Subset of (oContMaps X,Y);
cluster pi A,x -> non empty ;
coherence
not pi A,x is empty
proof end;
end;

theorem Th4: :: WAYBEL26:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Omega Sierpinski_Space is TopAugmentation of BoolePoset 1
proof end;

theorem Th5: :: WAYBEL26:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace ex f being Function of (InclPoset the topology of X),(oContMaps X,Sierpinski_Space ) st
( f is isomorphic & ( for V being open Subset of X holds f . V = chi V,the carrier of X ) )
proof end;

theorem Th6: :: WAYBEL26:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds InclPoset the topology of X, oContMaps X,Sierpinski_Space are_isomorphic
proof end;

definition
let X, Y, Z be non empty TopSpace;
let f be continuous Function of Y,Z;
func oContMaps X,f -> Function of (oContMaps X,Y),(oContMaps X,Z) means :Def2: :: WAYBEL26:def 2
for g being continuous Function of X,Y holds it . g = f * g;
uniqueness
for b1, b2 being Function of (oContMaps X,Y),(oContMaps X,Z) st ( for g being continuous Function of X,Y holds b1 . g = f * g ) & ( for g being continuous Function of X,Y holds b2 . g = f * g ) holds
b1 = b2
proof end;
existence
ex b1 being Function of (oContMaps X,Y),(oContMaps X,Z) st
for g being continuous Function of X,Y holds b1 . g = f * g
proof end;
func oContMaps f,X -> Function of (oContMaps Z,X),(oContMaps Y,X) means :Def3: :: WAYBEL26:def 3
for g being continuous Function of Z,X holds it . g = g * f;
uniqueness
for b1, b2 being Function of (oContMaps Z,X),(oContMaps Y,X) st ( for g being continuous Function of Z,X holds b1 . g = g * f ) & ( for g being continuous Function of Z,X holds b2 . g = g * f ) holds
b1 = b2
proof end;
existence
ex b1 being Function of (oContMaps Z,X),(oContMaps Y,X) st
for g being continuous Function of Z,X holds b1 . g = g * f
proof end;
end;

:: deftheorem Def2 defines oContMaps WAYBEL26:def 2 :
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps X,Y),(oContMaps X,Z) holds
( b5 = oContMaps X,f iff for g being continuous Function of X,Y holds b5 . g = f * g );

:: deftheorem Def3 defines oContMaps WAYBEL26:def 3 :
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps Z,X),(oContMaps Y,X) holds
( b5 = oContMaps f,X iff for g being continuous Function of Z,X holds b5 . g = g * f );

theorem Th7: :: WAYBEL26:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds oContMaps X,Y is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL25:43;

theorem Th8: :: WAYBEL26:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds oContMaps X,Y is up-complete
proof end;

theorem Th9: :: WAYBEL26:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps X,f is monotone
proof end;

theorem :: WAYBEL26:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps X,f is idempotent
proof end;

theorem Th11: :: WAYBEL26:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps f,X is monotone
proof end;

theorem Th12: :: WAYBEL26:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps f,X is idempotent
proof end;

theorem Th13: :: WAYBEL26:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of X
for A being Subset of (oContMaps X,Y) holds pi ((oContMaps X,f) .: A),x = f .: (pi A,x)
proof end;

theorem Th14: :: WAYBEL26:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps X,f is directed-sups-preserving
proof end;

theorem Th15: :: WAYBEL26:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of Y
for A being Subset of (oContMaps Z,X) holds pi ((oContMaps f,X) .: A),x = pi A,(f . x)
proof end;

theorem Th16: :: WAYBEL26:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, Z being non empty TopSpace
for X being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps f,X is directed-sups-preserving
proof end;

theorem Th17: :: WAYBEL26:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Z being non empty TopSpace
for Y being non empty SubSpace of Z holds oContMaps X,Y is full SubRelStr of oContMaps X,Z
proof end;

theorem Th18: :: WAYBEL26:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
proof end;

Lm1: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is_a_retraction holds
Y is monotone-convergence
proof end;

theorem Th19: :: WAYBEL26:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is_a_retraction holds
oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
proof end;

theorem Th20: :: WAYBEL26:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps X,Y is_a_retract_of oContMaps X,Z
proof end;

theorem Th21: :: WAYBEL26:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z st f is_homeomorphism holds
oContMaps X,f is isomorphic
proof end;

theorem Th22: :: WAYBEL26:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being non empty TopSpace st Y,Z are_homeomorphic holds
oContMaps X,Y, oContMaps X,Z are_isomorphic
proof end;

theorem Th23: :: WAYBEL26:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps X,Z is complete & oContMaps X,Z is continuous holds
( oContMaps X,Y is complete & oContMaps X,Y is continuous )
proof end;

theorem Th24: :: WAYBEL26:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps X,Z is complete & oContMaps X,Z is continuous holds
( oContMaps X,Y is complete & oContMaps X,Y is continuous )
proof end;

theorem Th25: :: WAYBEL26:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non trivial T_0-TopSpace st not Y is_T1 holds
Sierpinski_Space is_Retract_of Y
proof end;

theorem Th26: :: WAYBEL26:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being non trivial T_0-TopSpace st oContMaps X,Y is with_suprema holds
not Y is_T1
proof end;

registration
cluster Sierpinski_Space -> non trivial monotone-convergence ;
coherence
( not Sierpinski_Space is trivial & Sierpinski_Space is monotone-convergence )
proof end;
end;

registration
cluster non trivial injective monotone-convergence TopStruct ;
existence
ex b1 being T_0-TopSpace st
( b1 is injective & b1 is monotone-convergence & not b1 is trivial )
proof end;
end;

theorem Th27: :: WAYBEL26:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps X,Y is complete & oContMaps X,Y is continuous holds
InclPoset the topology of X is continuous
proof end;

theorem Th28: :: WAYBEL26:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for x being Point of X
for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps X,Y),(oContMaps X,Y) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps h,Y ) )
proof end;

theorem Th29: :: WAYBEL26:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace st oContMaps X,Y is complete & oContMaps X,Y is continuous holds
( Omega Y is complete & Omega Y is continuous )
proof end;

theorem Th30: :: WAYBEL26:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty 1-sorted
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj J,i) * f
proof end;

theorem Th31: :: WAYBEL26:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 1-sorted
for M being set holds Carrier (M --> S) = M --> the carrier of S
proof end;

theorem Th32: :: WAYBEL26:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for M being non empty set
for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M,the carrier of (oContMaps X,Y)
proof end;

theorem Th33: :: WAYBEL26:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace holds the carrier of (oContMaps X,Y) c= Funcs the carrier of X,the carrier of Y
proof end;

theorem Th34: :: WAYBEL26:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for M being non empty set
for f being Function of M,the carrier of (oContMaps X,Y) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
proof end;

theorem Th35: :: WAYBEL26:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for M being non empty set ex F being Function of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))),(M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )) holds F . f = commute f ) )
proof end;

theorem Th36: :: WAYBEL26:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for M being non empty set holds oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )),M -POS_prod (M --> (oContMaps X,Sierpinski_Space )) are_isomorphic
proof end;

theorem Th37: :: WAYBEL26:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st InclPoset the topology of X is continuous holds
for Y being injective T_0-TopSpace holds
( oContMaps X,Y is complete & oContMaps X,Y is continuous )
proof end;

registration
cluster Scott complete non trivial TopRelStr ;
existence
ex b1 being TopLattice st
( not b1 is trivial & b1 is complete & b1 is Scott )
proof end;
end;

theorem :: WAYBEL26:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for L being Scott complete non trivial TopLattice holds
( oContMaps X,L is complete & oContMaps X,L is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
proof end;

registration
let f be Function;
cluster Union (disjoin f) -> Relation-like ;
coherence
Union (disjoin f) is Relation-like
proof end;
end;

definition
let f be Function;
func *graph f -> Relation equals :: WAYBEL26:def 4
(Union (disjoin f)) ~ ;
correctness
coherence
(Union (disjoin f)) ~ is Relation
;
;
end;

:: deftheorem defines *graph WAYBEL26:def 4 :
for f being Function holds *graph f = (Union (disjoin f)) ~ ;

theorem Th39: :: WAYBEL26:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being Function holds
( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
proof end;

theorem Th40: :: WAYBEL26:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set holds
( proj1 X is finite & proj2 X is finite )
proof end;

theorem Th41: :: WAYBEL26:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
proof end;

definition
let W be Relation;
let X be set ;
func W,X *graph -> Function means :Def5: :: WAYBEL26:def 5
( dom it = X & ( for x being set st x in X holds
it . x = W .: {x} ) );
existence
ex b1 being Function st
( dom b1 = X & ( for x being set st x in X holds
b1 . x = W .: {x} ) )
proof end;
correctness
uniqueness
for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds
b1 . x = W .: {x} ) & dom b2 = X & ( for x being set st x in X holds
b2 . x = W .: {x} ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines *graph WAYBEL26:def 5 :
for W being Relation
for X being set
for b3 being Function holds
( b3 = W,X *graph iff ( dom b3 = X & ( for x being set st x in X holds
b3 . x = W .: {x} ) ) );

theorem Th42: :: WAYBEL26:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Relation
for X being set st dom W c= X holds
*graph (W,X *graph ) = W
proof end;

registration
let X, Y be TopSpace;
cluster -> Relation-like Element of bool the carrier of [:X,Y:];
coherence
for b1 being Subset of [:X,Y:] holds b1 is Relation-like
proof end;
cluster -> Relation-like Element of the topology of [:X,Y:];
coherence
for b1 being Element of the topology of [:X,Y:] holds b1 is Relation-like
proof end;
end;

theorem Th43: :: WAYBEL26:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for W being open Subset of [:X,Y:]
for x being Point of X holds W .: {x} is open Subset of Y
proof end;

theorem Th44: :: WAYBEL26:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:] holds W,the carrier of X *graph is continuous Function of X,S
proof end;

theorem Th45: :: WAYBEL26:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds
for f1, f2 being Element of (oContMaps X,S) st f1 = W1,the carrier of X *graph & f2 = W2,the carrier of X *graph holds
f1 <= f2
proof end;

theorem :: WAYBEL26:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph ) )
proof end;