let a, b be Real; for A being Subset of R^1 st A = [.a,b.] holds
A is closed
let A be Subset of R^1; ( A = [.a,b.] implies A is closed )
assume A1:
A = [.a,b.]
; A is closed
reconsider B = A ` as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def 6;
reconsider a = a, b = b as Real ;
reconsider D = B as Subset of RealSpace by TOPMETR:12;
set C = D ` ;
A2:
the carrier of RealSpace = the carrier of (TopSpaceMetr RealSpace)
by TOPMETR:12;
for c being Point of RealSpace st c in B holds
ex r being Real st
( r > 0 & Ball (c,r) c= B )
proof
let c be
Point of
RealSpace;
( c in B implies ex r being Real st
( r > 0 & Ball (c,r) c= B ) )
reconsider n =
c as
Element of
REAL by METRIC_1:def 13;
assume
c in B
;
ex r being Real st
( r > 0 & Ball (c,r) c= B )
then
not
n in [.a,b.]
by A1, XBOOLE_0:def 5;
then A3:
not
n in { p where p is Real : ( a <= p & p <= b ) }
by RCOMP_1:def 1;
now ex r being set st
( r > 0 & Ball (c,r) c= B )per cases
( not a <= n or not n <= b )
by A3;
suppose A4:
not
a <= n
;
ex r being set st
( r > 0 & Ball (c,r) c= B )take r =
a - n;
( r > 0 & Ball (c,r) c= B )now for x being object st x in Ball (c,r) holds
x in Blet x be
object ;
( x in Ball (c,r) implies x in B )assume A5:
x in Ball (
c,
r)
;
x in Bthen reconsider t =
x as
Element of
REAL by METRIC_1:def 13;
reconsider u =
x as
Point of
RealSpace by A5;
Ball (
c,
r)
= { q where q is Element of RealSpace : dist (c,q) < r }
by METRIC_1:17;
then
ex
v being
Element of
RealSpace st
(
v = u &
dist (
c,
v)
< r )
by A5;
then
real_dist . (
t,
n)
< r
by METRIC_1:def 1, METRIC_1:def 13;
then A6:
|.(t - n).| < r
by METRIC_1:def 12;
t - n <= |.(t - n).|
by ABSVALUE:4;
then
t - n < a - n
by A6, XXREAL_0:2;
then
for
q being
Real holds
( not
q = t or not
a <= q or not
q <= b )
by XREAL_1:9;
then
not
t in { p where p is Real : ( a <= p & p <= b ) }
;
then
not
u in D `
by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;
hence
x in B
by SUBSET_1:29;
verum end; hence
(
r > 0 &
Ball (
c,
r)
c= B )
by A4, XREAL_1:50;
verum end; suppose A7:
not
n <= b
;
ex r being set st
( r > 0 & Ball (c,r) c= B )take r =
n - b;
( r > 0 & Ball (c,r) c= B )now for x being object st x in Ball (c,r) holds
x in Blet x be
object ;
( x in Ball (c,r) implies x in B )assume A8:
x in Ball (
c,
r)
;
x in Bthen reconsider t =
x as
Element of
REAL by METRIC_1:def 13;
reconsider u =
x as
Point of
RealSpace by A8;
Ball (
c,
r)
= { q where q is Element of RealSpace : dist (c,q) < r }
by METRIC_1:17;
then
ex
v being
Element of
RealSpace st
(
v = u &
dist (
c,
v)
< r )
by A8;
then
real_dist . (
n,
t)
< r
by METRIC_1:def 1, METRIC_1:def 13;
then A9:
|.(n - t).| < r
by METRIC_1:def 12;
n - t <= |.(n - t).|
by ABSVALUE:4;
then
n - t < n - b
by A9, XXREAL_0:2;
then
for
q being
Real holds
( not
q = t or not
a <= q or not
q <= b )
by XREAL_1:10;
then
not
t in { p where p is Real : ( a <= p & p <= b ) }
;
then
not
u in D `
by A1, A2, RCOMP_1:def 1, TOPMETR:def 6;
hence
x in B
by SUBSET_1:29;
verum end; hence
(
r > 0 &
Ball (
c,
r)
c= B )
by A7, XREAL_1:50;
verum end; end; end;
hence
ex
r being
Real st
(
r > 0 &
Ball (
c,
r)
c= B )
;
verum
end;
then
A ` is open
by TOPMETR:15, TOPMETR:def 6;
hence
A is closed
by TOPS_1:3; verum