let n be Element of NAT ; for s1 being Real
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let s1 be Real; for P being Subset of (TOP-REAL n)
for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n holds
P is open
let i be Element of NAT ; ( P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n implies P is open )
assume A1:
( P = { p where p is Point of (TOP-REAL n) : s1 < p /. i } & i in Seg n )
; P is open
reconsider s1 = s1 as Real ;
A2:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider PP = P as Subset of (TopSpaceMetr (Euclid n)) ;
for pe being Point of (Euclid n) st pe in P holds
ex r being Real st
( r > 0 & Ball (pe,r) c= P )
proof
let pe be
Point of
(Euclid n);
( pe in P implies ex r being Real st
( r > 0 & Ball (pe,r) c= P ) )
assume
pe in P
;
ex r being Real st
( r > 0 & Ball (pe,r) c= P )
then consider p being
Point of
(TOP-REAL n) such that A3:
p = pe
and A4:
s1 < p /. i
by A1;
set r =
((p /. i) - s1) / 2;
A5:
(p /. i) - s1 > 0
by A4, XREAL_1:50;
Ball (
pe,
(((p /. i) - s1) / 2))
c= P
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (pe,(((p /. i) - s1) / 2)) or x in P )
assume
x in Ball (
pe,
(((p /. i) - s1) / 2))
;
x in P
then
x in { q where q is Element of (Euclid n) : dist (pe,q) < ((p /. i) - s1) / 2 }
by METRIC_1:17;
then consider q being
Element of
(Euclid n) such that A6:
q = x
and A7:
dist (
pe,
q)
< ((p /. i) - s1) / 2
;
reconsider ppe =
pe,
pq =
q as
Point of
(TOP-REAL n) by TOPREAL3:8;
reconsider pen =
ppe,
pqn =
pq as
Element of
REAL n ;
(Pitag_dist n) . (
pe,
q)
= dist (
pe,
q)
by METRIC_1:def 1;
then A8:
|.(pen - pqn).| < ((p /. i) - s1) / 2
by A7, EUCLID:def 6;
reconsider qq =
ppe - pq as
Element of
REAL n by EUCLID:22;
(ppe - pq) /. i <= |.qq.|
by A1, Th11;
then
(ppe - pq) /. i <= |.(pen - pqn).|
;
then
(ppe - pq) /. i < ((p /. i) - s1) / 2
by A8, XXREAL_0:2;
then
(ppe /. i) - (pq /. i) < ((p /. i) - s1) / 2
by A1, Th6;
then
((ppe /. i) - (pq /. i)) + (pq /. i) < (((p /. i) - s1) / 2) + (pq /. i)
by XREAL_1:6;
then A9:
(ppe /. i) - (((p /. i) - s1) / 2) < ((pq /. i) + (((p /. i) - s1) / 2)) - (((p /. i) - s1) / 2)
by XREAL_1:9;
(p /. i) - (((p /. i) - s1) / 2) = s1 + (((p /. i) - s1) / 2)
;
then
s1 < (p /. i) - (((p /. i) - s1) / 2)
by A5, XREAL_1:29, XREAL_1:139;
then
s1 < pq /. i
by A3, A9, XXREAL_0:2;
hence
x in P
by A1, A6;
verum
end;
hence
ex
r being
Real st
(
r > 0 &
Ball (
pe,
r)
c= P )
by A5, XREAL_1:139;
verum
end;
then
PP is open
by TOPMETR:15;
hence
P is open
by A2, PRE_TOPC:30; verum