begin
theorem Th1:
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem Th5:
:: deftheorem PCOMPS_1:def 1 :
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
:: deftheorem Def2 defines locally_finite PCOMPS_1:def 2 :
theorem Th11:
theorem Th12:
theorem Th13:
:: deftheorem Def3 defines clf PCOMPS_1:def 3 :
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem
:: deftheorem Def4 defines paracompact PCOMPS_1:def 4 :
theorem
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def5 defines Family_open_set PCOMPS_1:def 5 :
theorem Th29:
theorem Th30:
theorem
theorem
canceled;
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem defines TopSpaceMetr PCOMPS_1:def 6 :
theorem Th38:
definition
let D be
set ;
let f be
Function of
[:D,D:],
REAL ;
pred f is_metric_of D means :
Def7:
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:
:: deftheorem Def8 defines SpaceMetr PCOMPS_1:def 8 :
:: deftheorem defines metrizable PCOMPS_1:def 9 :
theorem