let M be non empty Reflexive symmetric triangle MetrStruct ; for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
set T = TopSpaceMetr M;
let r be Real; for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) holds
for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
let A be Subset of M; ( r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) implies for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite )
assume that
A1:
r > 0
and
A2:
for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r
; for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
A3:
r / 2 > 0
by A1, XREAL_1:215;
let F be Subset-Family of (TopSpaceMetr M); ( F = { {x} where x is Element of (TopSpaceMetr M) : x in A } implies F is locally_finite )
assume A4:
F = { {x} where x is Element of (TopSpaceMetr M) : x in A }
; F is locally_finite
let x be Point of (TopSpaceMetr M); PCOMPS_1:def 1 ex b1 being Element of bool the carrier of (TopSpaceMetr M) st
( x in b1 & b1 is open & { b2 where b2 is Element of bool the carrier of (TopSpaceMetr M) : ( b2 in F & not b2 misses b1 ) } is finite )
reconsider x9 = x as Point of M ;
reconsider B = Ball (x9,(r / 2)) as Subset of (TopSpaceMetr M) ;
take
B
; ( x in B & B is open & { b1 where b1 is Element of bool the carrier of (TopSpaceMetr M) : ( b1 in F & not b1 misses B ) } is finite )
A5:
dist (x9,x9) = 0
by METRIC_1:1;
B in Family_open_set M
by PCOMPS_1:29;
hence
( x in B & B is open )
by A5, A3, METRIC_1:11, PRE_TOPC:def 2; { b1 where b1 is Element of bool the carrier of (TopSpaceMetr M) : ( b1 in F & not b1 misses B ) } is finite
set VV = { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } ;
per cases
( for p being Point of M st p in A holds
dist (p,x9) >= r / 2 or ex p being Point of M st
( p in A & dist (p,x9) < r / 2 ) )
;
suppose
ex
p being
Point of
M st
(
p in A &
dist (
p,
x9)
< r / 2 )
;
{ b1 where b1 is Element of bool the carrier of (TopSpaceMetr M) : ( b1 in F & not b1 misses B ) } is finite then consider p being
Point of
M such that A12:
p in A
and A13:
dist (
p,
x9)
< r / 2
;
{ V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } c= {{p}}
proof
let v be
object ;
TARSKI:def 3 ( not v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } or v in {{p}} )
assume
v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) }
;
v in {{p}}
then consider V being
Subset of
(TopSpaceMetr M) such that A14:
v = V
and A15:
V in F
and A16:
V meets B
;
consider y being
Point of
(TopSpaceMetr M) such that A17:
V = {y}
and A18:
y in A
by A4, A15;
reconsider y =
y as
Point of
M ;
y in B
by A16, A17, ZFMISC_1:50;
then
dist (
x9,
y)
< r / 2
by METRIC_1:11;
then A19:
(dist (p,x9)) + (dist (x9,y)) < (r / 2) + (r / 2)
by A13, XREAL_1:8;
dist (
p,
y)
<= (dist (p,x9)) + (dist (x9,y))
by METRIC_1:4;
then
dist (
p,
y)
< (r / 2) + (r / 2)
by A19, XXREAL_0:2;
then
p = y
by A2, A12, A18;
hence
v in {{p}}
by A14, A17, TARSKI:def 1;
verum
end; hence
{ b1 where b1 is Element of bool the carrier of (TopSpaceMetr M) : ( b1 in F & not b1 misses B ) } is
finite
;
verum end; end;