let r, s be Real; for jauge being Function of [.r,s.],].0,+infty.[
for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is open
let jauge be Function of [.r,s.],].0,+infty.[; for S being Subset-Family of (Closed-Interval-TSpace (r,s)) st r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } holds
S is open
let S be Subset-Family of (Closed-Interval-TSpace (r,s)); ( r <= s & S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum } implies S is open )
assume that
A1:
r <= s
and
A2:
S = { (].(x - (jauge . x)),(x + (jauge . x)).[ /\ [.r,s.]) where x is Element of [.r,s.] : verum }
; S is open
for P being Subset of (Closed-Interval-TSpace (r,s)) st P in S holds
P is open
proof
let P be
Subset of
(Closed-Interval-TSpace (r,s));
( P in S implies P is open )
assume
P in S
;
P is open
then consider x0 being
Element of
[.r,s.] such that A4:
P = ].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ /\ [.r,s.]
by A2;
set CIT =
Closed-Interval-TSpace (
r,
s);
set CIM =
Closed-Interval-MSpace (
r,
s);
A5:
Closed-Interval-TSpace (
r,
s)
= TopSpaceMetr (Closed-Interval-MSpace (r,s))
by TOPMETR:def 7;
A6:
TopSpaceMetr (Closed-Interval-MSpace (r,s)) = TopStruct(# the
carrier of
(Closed-Interval-MSpace (r,s)),
(Family_open_set (Closed-Interval-MSpace (r,s))) #)
by PCOMPS_1:def 5;
reconsider I =
[.r,s.] as non
empty Subset of
RealSpace by A1, XXREAL_1:30;
reconsider P1 =
P as
Subset of
(Closed-Interval-MSpace (r,s)) by TOPMETR:def 7, A6;
for
t being
Element of
(Closed-Interval-MSpace (r,s)) st
t in P1 holds
ex
r being
Real st
(
r > 0 &
Ball (
t,
r)
c= P1 )
proof
let t be
Element of
(Closed-Interval-MSpace (r,s));
( t in P1 implies ex r being Real st
( r > 0 & Ball (t,r) c= P1 ) )
assume A7:
t in P1
;
ex r being Real st
( r > 0 & Ball (t,r) c= P1 )
the
carrier of
(Closed-Interval-MSpace (r,s)) c= the
carrier of
RealSpace
by TOPMETR:def 1;
then reconsider tr =
t as
Point of
RealSpace ;
reconsider XJ =
].(x0 - (jauge . x0)),(x0 + (jauge . x0)).[ as
Subset of
RealSpace ;
reconsider XK =
XJ as
Subset of
R^1 by TOPMETR:17;
not
[.r,s.] is
empty
by A1, XXREAL_1:30;
then
x0 in [.r,s.]
;
then reconsider p =
x0 as
Point of
RealSpace ;
tr in XK
by A7, A4, XBOOLE_0:def 4;
then consider r0 being
Real such that A8:
r0 > 0
and A9:
Ball (
tr,
r0)
c= XK
by JORDAN6:35, TOPMETR:15, TOPMETR:def 6;
take
r0
;
( r0 > 0 & Ball (t,r0) c= P1 )
Ball (
t,
r0)
= (Ball (tr,r0)) /\ the
carrier of
(Closed-Interval-MSpace (r,s))
by TOPMETR:9;
then
Ball (
t,
r0)
= (Ball (tr,r0)) /\ [.r,s.]
by A1, TOPMETR:10;
hence
(
r0 > 0 &
Ball (
t,
r0)
c= P1 )
by A4, A8, A9, XBOOLE_1:27;
verum
end;
then
P in Family_open_set (Closed-Interval-MSpace (r,s))
by PCOMPS_1:def 4;
hence
P is
open
by A5, A6, PRE_TOPC:def 2;
verum
end;
hence
S is open
by TOPS_2:def 1; verum