let n be Nat; for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ( PP = product_prebasis ((Seg n) --> R^1) implies PP is open )
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
set T = TopSpaceMetr (Euclid n);
set E = Euclid n;
assume A1:
PP = product_prebasis ((Seg n) --> R^1)
; PP is open
let x be Subset of (TopSpaceMetr (Euclid n)); TOPS_2:def 1 ( not x in PP or x is open )
assume
x in PP
; x is open
then consider i being set , R being TopStruct , V being Subset of R such that
A2:
i in Seg n
and
A3:
V is open
and
A4:
R = ((Seg n) --> R^1) . i
and
A5:
x = product ((Carrier ((Seg n) --> R^1)) +* (i,V))
by A1, WAYBEL18:def 2;
A6:
dom (Carrier ((Seg n) --> R^1)) = Seg n
by PARTFUN1:def 2;
A7:
now for i being set
for e, y being Point of (Euclid n)
for r being Real st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))let i be
set ;
for e, y being Point of (Euclid n)
for r being Real st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))let e,
y be
Point of
(Euclid n);
for r being Real st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))let r be
Real;
( y in Ball (e,r) implies y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) )assume A8:
y in Ball (
e,
r)
;
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))set O =
].((e . i) - r),((e . i) + r).[;
set G =
(Carrier ((Seg n) --> R^1)) +* (
i,
].((e . i) - r),((e . i) + r).[);
A9:
dom y = Seg n
by FINSEQ_1:89;
A10:
dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
now for a being object st a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) holds
y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . alet a be
object ;
( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 )assume A11:
a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
;
y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1per cases
( a = i or a <> i )
;
suppose A12:
a = i
;
y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1A13:
y . i = (e . i) + ((y . i) - (e . i))
;
A14:
dom e = Seg n
by FINSEQ_1:89;
dom (y - e) = (dom y) /\ (dom e)
by VALUED_1:12;
then A15:
(y - e) . i = (y . i) - (e . i)
by A9, A14, A11, A12, A10, VALUED_1:13;
|.((y - e) . i).| < r
by A8, Th10;
then
y . i in ].((e . i) - r),((e . i) + r).[
by A15, A13, FCONT_3:3;
hence
y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a
by A12, A10, A11, FUNCT_7:31;
verum end; suppose
a <> i
;
y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1then A16:
((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a
by FUNCT_7:32;
A17:
ex
R being
1-sorted st
(
R = ((Seg n) --> R^1) . a &
(Carrier ((Seg n) --> R^1)) . a = the
carrier of
R )
by A11, A10, PRALG_1:def 15;
y . a in REAL
by XREAL_0:def 1;
hence
y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a
by A16, A11, A10, A17, FUNCOP_1:7;
verum end; end; end; hence
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
by A10, A6, A9, CARD_3:9;
verum end;
set F = (Carrier ((Seg n) --> R^1)) +* (i,V);
A18:
R = R^1
by A2, A4, FUNCOP_1:7;
for e being Element of (Euclid n) st e in x holds
ex r being Real st
( r > 0 & Ball (e,r) c= x )
proof
let e be
Element of
(Euclid n);
( e in x implies ex r being Real st
( r > 0 & Ball (e,r) c= x ) )
assume A19:
e in x
;
ex r being Real st
( r > 0 & Ball (e,r) c= x )
A20:
dom ((Carrier ((Seg n) --> R^1)) +* (i,V)) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
then A21:
e . i in ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i
by A2, A6, A19, A5, CARD_3:9;
A22:
((Carrier ((Seg n) --> R^1)) +* (i,V)) . i = V
by A2, A6, FUNCT_7:31;
then consider r being
Real such that A23:
r > 0
and A24:
].((e . i) - r),((e . i) + r).[ c= V
by A3, A18, A21, FRECHET:8;
take
r
;
( r > 0 & Ball (e,r) c= x )
thus
r > 0
by A23;
Ball (e,r) c= x
let y be
object ;
TARSKI:def 3 ( not y in Ball (e,r) or y in x )
assume A25:
y in Ball (
e,
r)
;
y in x
then reconsider y =
y as
Point of
(Euclid n) ;
set O =
].((e . i) - r),((e . i) + r).[;
set G =
(Carrier ((Seg n) --> R^1)) +* (
i,
].((e . i) - r),((e . i) + r).[);
A26:
dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1))
by FUNCT_7:30;
A27:
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
by A25, A7;
now for a being object st a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) holds
((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . alet a be
object ;
( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 )assume A28:
a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
;
((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 end;
then
product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) c= product ((Carrier ((Seg n) --> R^1)) +* (i,V))
by A20, CARD_3:27, FUNCT_7:30;
hence
y in x
by A27, A5;
verum
end;
then
x in the topology of (TopSpaceMetr (Euclid n))
by PCOMPS_1:def 4;
hence
x is open
by PRE_TOPC:def 2; verum