:: Paracompact and Metrizable Spaces
:: by Leszek Borys
::
:: Received June 8, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: PCOMPS_1:1
theorem Th2: :: PCOMPS_1:2
theorem :: PCOMPS_1:3
canceled;
theorem :: PCOMPS_1:4
canceled;
theorem Th5: :: PCOMPS_1:5
:: deftheorem PCOMPS_1:def 1 :
canceled;
theorem :: PCOMPS_1:6
canceled;
theorem :: PCOMPS_1:7
theorem :: PCOMPS_1:8
theorem :: PCOMPS_1:9
theorem :: PCOMPS_1:10
:: deftheorem Def2 defines locally_finite PCOMPS_1:def 2 :
theorem Th11: :: PCOMPS_1:11
theorem Th12: :: PCOMPS_1:12
theorem Th13: :: PCOMPS_1:13
:: deftheorem Def3 defines clf PCOMPS_1:def 3 :
theorem :: PCOMPS_1:14
theorem Th15: :: PCOMPS_1:15
theorem Th16: :: PCOMPS_1:16
theorem Th17: :: PCOMPS_1:17
theorem Th18: :: PCOMPS_1:18
theorem Th19: :: PCOMPS_1:19
theorem Th20: :: PCOMPS_1:20
theorem :: PCOMPS_1:21
theorem :: PCOMPS_1:22
theorem Th23: :: PCOMPS_1:23
theorem :: PCOMPS_1:24
:: deftheorem Def4 defines paracompact PCOMPS_1:def 4 :
theorem :: PCOMPS_1:25
theorem Th26: :: PCOMPS_1:26
theorem Th27: :: PCOMPS_1:27
theorem :: PCOMPS_1:28
:: deftheorem Def5 defines Family_open_set PCOMPS_1:def 5 :
theorem Th29: :: PCOMPS_1:29
theorem Th30: :: PCOMPS_1:30
theorem :: PCOMPS_1:31
theorem :: PCOMPS_1:32
canceled;
theorem Th33: :: PCOMPS_1:33
theorem Th34: :: PCOMPS_1:34
theorem Th35: :: PCOMPS_1:35
theorem Th36: :: PCOMPS_1:36
theorem Th37: :: PCOMPS_1:37
:: deftheorem defines TopSpaceMetr PCOMPS_1:def 6 :
theorem Th38: :: PCOMPS_1:38
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
:: deftheorem Def8 defines SpaceMetr PCOMPS_1:def 8 :
:: deftheorem defines metrizable PCOMPS_1:def 9 :