let M be non empty MetrSpace; for X being Subset of M
for Y being Subset of (TopSpaceMetr M)
for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let X be Subset of M; for Y being Subset of (TopSpaceMetr M)
for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let Y be Subset of (TopSpaceMetr M); for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let x be Element of M; for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let y be Element of (TopSpaceMetr M); ( X = Y & x = y implies ( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) )
assume A1:
( X = Y & x = y )
; ( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
hereby ( ( for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) implies y is_an_accumulation_point_of Y )
assume
y is_an_accumulation_point_of Y
;
for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}then A2:
y in Der Y
by TOPGEN_1:16;
let r be
Real;
( 0 < r implies Ball (x,r) meets X \ {x} )assume A3:
0 < r
;
Ball (x,r) meets X \ {x}reconsider U =
Ball (
x,
r) as
Subset of
(TopSpaceMetr M) ;
A4:
U is
open
by TOPMETR:14;
dist (
x,
x)
= 0
by METRIC_1:1;
then consider z being
Point of
(TopSpaceMetr M) such that A5:
(
z in Y /\ U &
y <> z )
by A1, A2, A3, A4, METRIC_1:11, TOPGEN_1:17;
(
z in Y &
z in U & not
z in {y} )
by A5, TARSKI:def 1, XBOOLE_0:def 4;
then
(
z in Y \ {y} &
z in U )
by XBOOLE_0:def 5;
hence
Ball (
x,
r)
meets X \ {x}
by A1, XBOOLE_0:def 4;
verum
end;
assume A6:
for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}
; y is_an_accumulation_point_of Y
for U being open Subset of (TopSpaceMetr M) st y in U holds
ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z )
proof
let U be
open Subset of
(TopSpaceMetr M);
( y in U implies ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z ) )
assume A7:
y in U
;
ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z )
U is
open
;
then consider r being
Real such that A8:
(
0 < r &
Ball (
x,
r)
c= U )
by A1, A7, PCOMPS_1:def 4;
Ball (
x,
r)
meets X \ {x}
by A6, A8;
then consider z being
object such that A9:
z in (Ball (x,r)) /\ (X \ {x})
by XBOOLE_0:def 1;
(
z in Ball (
x,
r) &
z in X \ {x} )
by A9, XBOOLE_0:def 4;
then A10:
(
z in U &
z in Y & not
z in {x} )
by A1, A8, XBOOLE_0:def 5;
reconsider z =
z as
Point of
(TopSpaceMetr M) by A9;
take
z
;
( z in Y /\ U & y <> z )
thus
(
z in Y /\ U &
y <> z )
by A1, A10, TARSKI:def 1, XBOOLE_0:def 4;
verum
end;
then
y in Der Y
by TOPGEN_1:17;
hence
y is_an_accumulation_point_of Y
by TOPGEN_1:16; verum