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

theorem Th1: :: PCOMPS_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for x being Element of PM
for r, p being real number st r <= p holds
Ball x,r c= Ball x,p
proof end;

theorem Th2: :: PCOMPS_1:2  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 A being Subset of T holds
( Cl A <> {} iff A <> {} )
proof end;

theorem :: PCOMPS_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PCOMPS_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: PCOMPS_1:5  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
for FX being Subset-Family of T st FX is_a_cover_of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )
proof end;

definition
let X be set ;
:: original: bool
redefine func bool X -> Subset-Family of X;
coherence
bool X is Subset-Family of X
by ZFMISC_1:def 1;
end;

definition
let D be set ;
func 1TopSp D -> TopStruct equals :: PCOMPS_1:def 1
TopStruct(# D,(bool D) #);
coherence
TopStruct(# D,(bool D) #) is TopStruct
;
end;

:: deftheorem defines 1TopSp PCOMPS_1:def 1 :
for D being set holds 1TopSp D = TopStruct(# D,(bool D) #);

registration
let D be set ;
cluster 1TopSp D -> strict TopSpace-like ;
coherence
( 1TopSp D is strict & 1TopSp D is TopSpace-like )
proof end;
end;

registration
let D be non empty set ;
cluster 1TopSp D -> non empty strict TopSpace-like ;
coherence
not 1TopSp D is empty
;
end;

theorem :: PCOMPS_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PCOMPS_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds the topology of (1TopSp a) = bool a ;

theorem :: PCOMPS_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds the carrier of (1TopSp a) = a ;

theorem Th9: :: PCOMPS_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being set holds 1TopSp {a} is compact
proof end;

theorem Th10: :: PCOMPS_1:10  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
for x being Point of T st T is_T2 holds
{x} is closed
proof end;

definition
let T be TopStruct ;
let IT be Subset-Family of T;
attr IT is locally_finite means :Def2: :: PCOMPS_1:def 2
for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite );
end;

:: deftheorem Def2 defines locally_finite PCOMPS_1:def 2 :
for T being TopStruct
for IT being Subset-Family of T holds
( IT is locally_finite iff for x being Point of T ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in IT & V meets W ) } is finite ) );

theorem Th11: :: PCOMPS_1:11  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
for FX being Subset-Family of T
for W being Subset of T holds { V where V is Subset of T : ( V in FX & V meets W ) } c= FX
proof end;

theorem Th12: :: PCOMPS_1:12  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
for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
proof end;

theorem Th13: :: PCOMPS_1:13  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
for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
proof end;

definition
let T be TopStruct ;
let FX be Subset-Family of T;
func clf FX -> Subset-Family of T means :Def3: :: PCOMPS_1:def 3
for Z being Subset of T holds
( Z in it iff ex W being Subset of T st
( Z = Cl W & W in FX ) );
existence
ex b1 being Subset-Family of T st
for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of T st ( for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in b2 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines clf PCOMPS_1:def 3 :
for T being TopStruct
for FX, b3 being Subset-Family of T holds
( b3 = clf FX iff for Z being Subset of T holds
( Z in b3 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) );

theorem :: PCOMPS_1:14  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 FX being Subset-Family of T holds clf FX is closed
proof end;

theorem Th15: :: PCOMPS_1:15  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 FX being Subset-Family of T st FX = {} holds
clf FX = {}
proof end;

theorem Th16: :: PCOMPS_1:16  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
for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
proof end;

theorem Th17: :: PCOMPS_1:17  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
for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
proof end;

theorem Th18: :: PCOMPS_1:18  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
for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
proof end;

theorem Th19: :: PCOMPS_1:19  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
for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
proof end;

theorem Th20: :: PCOMPS_1:20  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
for FX being Subset-Family of T holds FX is_finer_than clf FX
proof end;

scheme :: PCOMPS_1:sch 1
Lambda1top{ F1() -> TopSpace, F2() -> Subset-Family of F1(), F3() -> Subset-Family of F1(), F4( set ) -> Subset of F1() } :
ex f being Function of F2(),F3() st
for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
provided
A1: for Z being Subset of F1() st Z in F2() holds
F4(Z) in F3()
proof end;

theorem :: PCOMPS_1:21  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
for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
proof end;

theorem Th22: :: PCOMPS_1:22  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
for FX being Subset-Family of T holds union FX c= union (clf FX)
proof end;

theorem Th23: :: PCOMPS_1:23  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
for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
proof end;

theorem :: PCOMPS_1:24  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
for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
proof end;

definition
let IT be TopStruct ;
attr IT is paracompact means :Def4: :: PCOMPS_1:def 4
for FX being Subset-Family of IT st FX is_a_cover_of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is_a_cover_of IT & GX is_finer_than FX & GX is locally_finite );
end;

:: deftheorem Def4 defines paracompact PCOMPS_1:def 4 :
for IT being TopStruct holds
( IT is paracompact iff for FX being Subset-Family of IT st FX is_a_cover_of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is_a_cover_of IT & GX is_finer_than FX & GX is locally_finite ) );

registration
cluster non empty paracompact TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is paracompact
proof end;
end;

theorem :: PCOMPS_1:25  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 compact holds
T is paracompact
proof end;

theorem Th26: :: PCOMPS_1:26  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
for A, B being Subset of T st T is paracompact & A is closed & B is closed & A misses B & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
proof end;

theorem Th27: :: PCOMPS_1:27  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_T2 & T is paracompact holds
T is_T3
proof end;

theorem :: PCOMPS_1:28  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_T2 & T is paracompact holds
T is_T4
proof end;

definition
let PM be MetrStruct ;
func Family_open_set PM -> Subset-Family of PM means :Def5: :: PCOMPS_1:def 5
for V being Subset of PM holds
( V in it iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V ) );
existence
ex b1 being Subset-Family of PM st
for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of PM st ( for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V ) ) ) & ( for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Family_open_set PCOMPS_1:def 5 :
for PM being MetrStruct
for b2 being Subset-Family of PM holds
( b2 = Family_open_set PM iff for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V ) ) );

theorem Th29: :: PCOMPS_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for x being Element of PM ex r being Real st
( r > 0 & Ball x,r c= the carrier of PM )
proof end;

theorem Th30: :: PCOMPS_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for y, x being Element of PM
for r being real number st PM is triangle & y in Ball x,r holds
ex p being Real st
( p > 0 & Ball y,p c= Ball x,r )
proof end;

theorem :: PCOMPS_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball x,r) /\ (Ball z,p) holds
ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
proof end;

theorem :: PCOMPS_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th33: :: PCOMPS_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for x being Element of PM
for r being real number st PM is triangle holds
Ball x,r in Family_open_set PM
proof end;

theorem Th34: :: PCOMPS_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct holds the carrier of PM in Family_open_set PM
proof end;

theorem Th35: :: PCOMPS_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
proof end;

theorem Th36: :: PCOMPS_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct
for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
proof end;

theorem Th37: :: PCOMPS_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being MetrStruct holds TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
proof end;

definition
let PM be MetrStruct ;
func TopSpaceMetr PM -> TopStruct equals :: PCOMPS_1:def 6
TopStruct(# the carrier of PM,(Family_open_set PM) #);
coherence
TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopStruct
;
end;

:: deftheorem defines TopSpaceMetr PCOMPS_1:def 6 :
for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);

registration
let PM be MetrStruct ;
cluster TopSpaceMetr PM -> strict TopSpace-like ;
coherence
( TopSpaceMetr PM is strict & TopSpaceMetr PM is TopSpace-like )
by Th37;
end;

registration
let PM be non empty MetrStruct ;
cluster TopSpaceMetr PM -> non empty strict TopSpace-like ;
coherence
not TopSpaceMetr PM is empty
;
end;

theorem Th38: :: PCOMPS_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PM being non empty MetrSpace holds TopSpaceMetr PM is_T2
proof end;

registration
cluster non empty strict being_T2 TopStruct ;
existence
ex b1 being TopSpace st
( b1 is being_T2 & not b1 is empty & b1 is strict )
proof end;
end;

definition
let D be set ;
let f be Function of [:D,D:], REAL ;
pred f is_metric_of D means :Def7: :: PCOMPS_1:def 7
for a, b, c being Element of D holds
( ( f . a,b = 0 implies a = b ) & ( a = b implies f . a,b = 0 ) & f . a,b = f . b,a & f . a,c <= (f . a,b) + (f . b,c) );
end;

:: deftheorem Def7 defines is_metric_of PCOMPS_1:def 7 :
for D being set
for f being Function of [:D,D:], REAL holds
( f is_metric_of D iff for a, b, c being Element of D holds
( ( f . a,b = 0 implies a = b ) & ( a = b implies f . a,b = 0 ) & f . a,b = f . b,a & f . a,c <= (f . a,b) + (f . b,c) ) );

theorem Th39: :: PCOMPS_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for f being Function of [:D,D:], REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
proof end;

definition
let D be non empty set ;
let f be Function of [:D,D:], REAL ;
assume A1: f is_metric_of D ;
func SpaceMetr D,f -> non empty strict MetrSpace equals :Def8: :: PCOMPS_1:def 8
MetrStruct(# D,f #);
coherence
MetrStruct(# D,f #) is non empty strict MetrSpace
by A1, Th39;
end;

:: deftheorem Def8 defines SpaceMetr PCOMPS_1:def 8 :
for D being non empty set
for f being Function of [:D,D:], REAL st f is_metric_of D holds
SpaceMetr D,f = MetrStruct(# D,f #);

definition
let IT be non empty TopStruct ;
attr IT is metrizable means :: PCOMPS_1:def 9
ex f being Function of [:the carrier of IT,the carrier of IT:], REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr the carrier of IT,f) = the topology of IT );
end;

:: deftheorem defines metrizable PCOMPS_1:def 9 :
for IT being non empty TopStruct holds
( IT is metrizable iff ex f being Function of [:the carrier of IT,the carrier of IT:], REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr the carrier of IT,f) = the topology of IT ) );

registration
cluster non empty strict metrizable TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is strict & b1 is metrizable )
proof end;
end;