let PM be non empty MetrStruct ; :: thesis: for r being real number st PM is non empty MetrSpace holds
for x being Element of PM holds ([#] PM) \ (cl_Ball x,r) in Family_open_set PM
let r be real number ; :: thesis: ( PM is non empty MetrSpace implies for x being Element of PM holds ([#] PM) \ (cl_Ball x,r) in Family_open_set PM )
reconsider r' = r as Real by XREAL_0:def 1;
assume A1:
PM is non empty MetrSpace
; :: thesis: for x being Element of PM holds ([#] PM) \ (cl_Ball x,r) in Family_open_set PM
let x be Element of PM; :: thesis: ([#] PM) \ (cl_Ball x,r) in Family_open_set PM
now let y be
Element of
PM;
:: thesis: ( y in ([#] PM) \ (cl_Ball x,r) implies ex r2 being Real st
( r2 > 0 & Ball y,r2 c= ([#] PM) \ (cl_Ball x,r) ) )assume
y in ([#] PM) \ (cl_Ball x,r)
;
:: thesis: ex r2 being Real st
( r2 > 0 & Ball y,r2 c= ([#] PM) \ (cl_Ball x,r) )then A2:
not
y in cl_Ball x,
r
by XBOOLE_0:def 5;
set r1 =
(dist x,y) - r';
r' + 0 < r' + ((dist x,y) - r')
by A2, METRIC_1:13;
then A3:
r' - r' < ((dist x,y) - r') - 0
by XREAL_1:23;
Ball y,
((dist x,y) - r') c= ([#] PM) \ (cl_Ball x,r)
proof
assume
not
Ball y,
((dist x,y) - r') c= ([#] PM) \ (cl_Ball x,r)
;
:: thesis: contradiction
then consider z being
set such that A4:
(
z in Ball y,
((dist x,y) - r') & not
z in ([#] PM) \ (cl_Ball x,r) )
by TARSKI:def 3;
reconsider z =
z as
Element of
PM by A4;
(
z in the
carrier of
PM &
z in Ball y,
((dist x,y) - r') & ( not
z in [#] PM or
z in cl_Ball x,
r ) )
by A4, XBOOLE_0:def 5;
then
(
dist y,
z < (dist x,y) - r' &
dist x,
z <= r' )
by METRIC_1:12, METRIC_1:13;
then
(dist y,z) + (dist x,z) < ((dist x,y) - r') + r'
by XREAL_1:10;
then
(dist x,z) + (dist z,y) < ((dist x,y) - r') + r'
by A1, METRIC_1:3;
hence
contradiction
by A1, METRIC_1:4;
:: thesis: verum
end; hence
ex
r2 being
Real st
(
r2 > 0 &
Ball y,
r2 c= ([#] PM) \ (cl_Ball x,r) )
by A3;
:: thesis: verum end;
hence
([#] PM) \ (cl_Ball x,r) in Family_open_set PM
by PCOMPS_1:def 5; :: thesis: verum