let n be Element of NAT ; :: thesis: for s1 being real number
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 < Proj p,i } & i in Seg n holds
P is open
let s1 be real number ; :: thesis: 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 < Proj p,i } & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); :: thesis: for i being Element of NAT st P = { p where p is Point of (TOP-REAL n) : s1 < Proj p,i } & i in Seg n holds
P is open
let i be Element of NAT ; :: thesis: ( P = { p where p is Point of (TOP-REAL n) : s1 < Proj p,i } & i in Seg n implies P is open )
assume A1:
( P = { p where p is Point of (TOP-REAL n) : s1 < Proj p,i } & i in Seg n )
; :: thesis: P is open
XX:
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)) ;
reconsider s1 = s1 as Real by XREAL_0:def 1;
for pe being Point of (Euclid n) st pe in P holds
ex r being real number st
( r > 0 & Ball pe,r c= P )
proof
let pe be
Point of
(Euclid n);
:: thesis: ( pe in P implies ex r being real number st
( r > 0 & Ball pe,r c= P ) )
assume
pe in P
;
:: thesis: ex r being real number st
( r > 0 & Ball pe,r c= P )
then consider p being
Point of
(TOP-REAL n) such that A2:
(
p = pe &
s1 < Proj p,
i )
by A1;
set r =
((Proj p,i) - s1) / 2;
(Proj p,i) - s1 > 0
by A2, XREAL_1:52;
then A3:
((Proj p,i) - s1) / 2
> 0
by XREAL_1:141;
Ball pe,
(((Proj p,i) - s1) / 2) c= P
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Ball pe,(((Proj p,i) - s1) / 2) or x in P )
assume
x in Ball pe,
(((Proj p,i) - s1) / 2)
;
:: thesis: x in P
then
x in { q where q is Element of (Euclid n) : dist pe,q < ((Proj p,i) - s1) / 2 }
by METRIC_1:18;
then consider q being
Element of
(Euclid n) such that A4:
q = x
and A5:
dist pe,
q < ((Proj p,i) - s1) / 2
;
reconsider ppe =
pe,
pq =
q as
Point of
(TOP-REAL n) by TOPREAL3:13;
reconsider pen =
ppe,
pqn =
pq as
Element of
REAL n ;
(Pitag_dist n) . pe,
q = dist pe,
q
by METRIC_1:def 1;
then A6:
|.(pen - pqn).| < ((Proj p,i) - s1) / 2
by A5, EUCLID:def 6;
reconsider qq =
ppe - pq as
Element of
REAL n by EUCLID:25;
X:
ppe - pq = pen - pqn
by A1, EUCLID:73;
Proj (ppe - pq),
i <= |.qq.|
by A1, Th15;
then
Proj (ppe - pq),
i <= |.(pen - pqn).|
by A1, EUCLID:73, X;
then
Proj (ppe - pq),
i < ((Proj p,i) - s1) / 2
by A6, XXREAL_0:2;
then
(Proj ppe,i) - (Proj pq,i) < ((Proj p,i) - s1) / 2
by A1, Th7;
then
((Proj ppe,i) - (Proj pq,i)) + (Proj pq,i) < (((Proj p,i) - s1) / 2) + (Proj pq,i)
by XREAL_1:8;
then A7:
(Proj ppe,i) - (((Proj p,i) - s1) / 2) < ((Proj pq,i) + (((Proj p,i) - s1) / 2)) - (((Proj p,i) - s1) / 2)
by XREAL_1:11;
(Proj p,i) - (((Proj p,i) - s1) / 2) = s1 + (((Proj p,i) - s1) / 2)
;
then
s1 < (Proj p,i) - (((Proj p,i) - s1) / 2)
by A3, XREAL_1:31;
then
(
pq = x &
s1 < Proj pq,
i )
by A2, A4, A7, XXREAL_0:2;
hence
x in P
by A1;
:: thesis: verum
end;
hence
ex
r being
real number st
(
r > 0 &
Ball pe,
r c= P )
by A3;
:: thesis: verum
end;
then
PP is open
by TOPMETR:22;
hence
P is open
by PRE_TOPC:60, XX; :: thesis: verum