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

theorem Th1: :: WAYBEL18:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z, Z being set holds
( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )
proof end;

Lm1: for X being set
for f, g being Function holds f " (g " X) = (g * f) " X
proof end;

theorem Th2: :: WAYBEL18:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A, B being Subset-Family of X st ( B = A \ {{} } or A = B \/ {{} } ) holds
UniCl A = UniCl B
proof end;

theorem Th3: :: WAYBEL18:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for K being Subset-Family of T holds
( K is Basis of T iff K \ {{} } is Basis of T )
proof end;

definition
let F be Relation;
attr F is TopSpace-yielding means :Def1: :: WAYBEL18:def 1
for x being set st x in rng F holds
x is TopStruct ;
end;

:: deftheorem Def1 defines TopSpace-yielding WAYBEL18:def 1 :
for F being Relation holds
( F is TopSpace-yielding iff for x being set st x in rng F holds
x is TopStruct );

registration
cluster TopSpace-yielding -> 1-sorted-yielding set ;
coherence
for b1 being Function st b1 is TopSpace-yielding holds
b1 is 1-sorted-yielding
proof end;
end;

registration
let I be set ;
cluster 1-sorted-yielding TopSpace-yielding ManySortedSet of I;
existence
ex b1 being ManySortedSet of I st b1 is TopSpace-yielding
proof end;
end;

registration
let I be set ;
cluster non-Empty 1-sorted-yielding TopSpace-yielding ManySortedSet of I;
existence
ex b1 being ManySortedSet of I st
( b1 is TopSpace-yielding & b1 is non-Empty )
proof end;
end;

definition
let J be non empty set ;
let A be TopSpace-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> TopStruct ;
coherence
A . j is TopStruct
proof end;
end;

definition
let I be set ;
let J be TopSpace-yielding ManySortedSet of I;
func product_prebasis J -> Subset-Family of (product (Carrier J)) means :Def2: :: WAYBEL18:def 2
for x being Subset of (product (Carrier J)) holds
( x in it iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) );
existence
ex b1 being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (product (Carrier J)) st ( for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) ) & ( for x being Subset of (product (Carrier J)) holds
( x in b2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
for I being set
for J being TopSpace-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier J)) holds
( b3 = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b3 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* i,V) ) ) );

theorem Th4: :: WAYBEL18:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof end;

definition
let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
func product J -> strict TopSpace means :Def3: :: WAYBEL18:def 3
( the carrier of it = product (Carrier J) & product_prebasis J is prebasis of it );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 )
proof end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 & the carrier of b2 = product (Carrier J) & product_prebasis J is prebasis of b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines product WAYBEL18:def 3 :
for I being set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for b3 being strict TopSpace holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & product_prebasis J is prebasis of b3 ) );

registration
let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
cluster product J -> non empty strict ;
coherence
not product J is empty
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func J . i -> non empty TopStruct ;
coherence
J . i is non empty TopStruct
proof end;
end;

registration
let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
cluster product J -> non empty strict constituted-Functions ;
coherence
product J is constituted-Functions
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine func x . i -> Element of (J . i);
coherence
x . i is Element of (J . i)
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
let i be Element of I;
func proj J,i -> Function of (product J),(J . i) equals :: WAYBEL18:def 4
proj (Carrier J),i;
coherence
proj (Carrier J),i is Function of (product J),(J . i)
proof end;
end;

:: deftheorem defines proj WAYBEL18:def 4 :
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj J,i = proj (Carrier J),i;

theorem Th5: :: WAYBEL18:5  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 non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (J . i) holds (proj J,i) " P = product ((Carrier J) +* i,P)
proof end;

theorem Th6: :: WAYBEL18:6  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 non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj J,i is continuous
proof end;

theorem Th7: :: WAYBEL18: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 I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj J,i) * f is continuous )
proof end;

definition
let Z be TopStruct ;
attr Z is injective means :Def5: :: WAYBEL18:def 5
for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f );
end;

:: deftheorem Def5 defines injective WAYBEL18:def 5 :
for Z being TopStruct holds
( Z is injective iff for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f ) );

theorem Th8: :: WAYBEL18:8  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 non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective
proof end;

theorem :: WAYBEL18:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is injective holds
for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
proof end;

definition
let X be 1-sorted ;
let Y be TopStruct ;
let f be Function of X,Y;
func Image f -> SubSpace of Y equals :: WAYBEL18:def 6
Y | (rng f);
coherence
Y | (rng f) is SubSpace of Y
;
end;

:: deftheorem defines Image WAYBEL18:def 6 :
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds Image f = Y | (rng f);

registration
let X be non empty 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster Image f -> non empty ;
coherence
not Image f is empty
proof end;
end;

theorem Th10: :: WAYBEL18:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f
proof end;

definition
let X be 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
func corestr f -> Function of X,(Image f) equals :: WAYBEL18:def 7
f;
coherence
f is Function of X,(Image f)
proof end;
end;

:: deftheorem defines corestr WAYBEL18:def 7 :
for X being 1-sorted
for Y being non empty TopStruct
for f being Function of X,Y holds corestr f = f;

theorem Th11: :: WAYBEL18:11  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 Function of X,Y st f is continuous holds
corestr f is continuous
proof end;

registration
let X be 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster corestr f -> onto ;
coherence
corestr f is onto
proof end;
end;

definition
let X, Y be TopStruct ;
pred X is_Retract_of Y means :: WAYBEL18:def 8
ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic );
end;

:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
for X, Y being TopStruct holds
( X is_Retract_of Y iff ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic ) );

theorem Th12: :: WAYBEL18:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S being non empty TopSpace st T is injective holds
for f being Function of T,S st corestr f is_homeomorphism holds
T is_Retract_of S
proof end;

definition
func Sierpinski_Space -> strict TopStruct means :Def9: :: WAYBEL18:def 9
( the carrier of it = {0,1} & the topology of it = {{} ,{1},{0,1}} );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = {0,1} & the topology of b1 = {{} ,{1},{0,1}} )
proof end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = {0,1} & the topology of b1 = {{} ,{1},{0,1}} & the carrier of b2 = {0,1} & the topology of b2 = {{} ,{1},{0,1}} holds
b1 = b2
;
end;

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :
for b1 being strict TopStruct holds
( b1 = Sierpinski_Space iff ( the carrier of b1 = {0,1} & the topology of b1 = {{} ,{1},{0,1}} ) );

registration
cluster Sierpinski_Space -> non empty strict TopSpace-like ;
coherence
( not Sierpinski_Space is empty & Sierpinski_Space is TopSpace-like )
proof end;
end;

Lm2: Sierpinski_Space is discerning
proof end;

registration
cluster Sierpinski_Space -> non empty strict TopSpace-like discerning ;
coherence
Sierpinski_Space is discerning
by Lm2;
end;

registration
cluster Sierpinski_Space -> non empty strict TopSpace-like discerning injective ;
coherence
Sierpinski_Space is injective
proof end;
end;

registration
let I be set ;
let S be non empty 1-sorted ;
cluster I --> S -> non-Empty ;
coherence
I --> S is non-Empty
proof end;
end;

registration
let I be set ;
let T be TopStruct ;
cluster I --> T -> 1-sorted-yielding TopSpace-yielding ;
coherence
I --> T is TopSpace-yielding
proof end;
end;

registration
let I be set ;
let L be reflexive RelStr ;
cluster I --> L -> reflexive-yielding ;
coherence
I --> L is reflexive-yielding
proof end;
end;

registration
let I be non empty set ;
let L be non empty antisymmetric RelStr ;
cluster product (I --> L) -> antisymmetric ;
coherence
product (I --> L) is antisymmetric
proof end;
end;

registration
let I be non empty set ;
let L be non empty transitive RelStr ;
cluster product (I --> L) -> transitive ;
coherence
product (I --> L) is transitive
proof end;
end;

theorem :: WAYBEL18:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Scott TopAugmentation of BoolePoset 1 holds the topology of T = the topology of Sierpinski_Space
proof end;

theorem Th14: :: WAYBEL18:14  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 holds { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } is prebasis of product (I --> Sierpinski_Space )
proof end;

registration
let I be non empty set ;
let L be complete LATTICE;
cluster product (I --> L) -> transitive antisymmetric with_suprema complete ;
coherence
( product (I --> L) is with_suprema & product (I --> L) is complete )
proof end;
end;

registration
let I be non empty set ;
let X be lower-bounded algebraic LATTICE;
cluster product (I --> X) -> transitive antisymmetric algebraic with_suprema complete ;
coherence
product (I --> X) is algebraic
proof end;
end;

theorem Th15: :: WAYBEL18:15  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 set ex f being Function of (BoolePoset X),(product (X --> (BoolePoset 1))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi Y,X ) )
proof end;

theorem Th16: :: WAYBEL18:16  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 T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the topology of T = the topology of (product (I --> Sierpinski_Space ))
proof end;

theorem Th17: :: WAYBEL18:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S being non empty TopSpace st the carrier of T = the carrier of S & the topology of T = the topology of S & T is injective holds
S is injective
proof end;

theorem :: WAYBEL18:18  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 T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds T is injective
proof end;

theorem Th19: :: WAYBEL18:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being T_0-TopSpace ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space )) st corestr f is_homeomorphism
proof end;

theorem :: WAYBEL18:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being T_0-TopSpace st T is injective holds
ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space )
proof end;