let n be Nat; :: thesis: 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)); :: thesis: ( 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) ; :: thesis: PP is open
let x be Subset of (TopSpaceMetr (Euclid n)); :: according to TOPS_2:def 1 :: thesis: ( not x in PP or x is open )
assume x in PP ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 :: thesis: 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).[)) . a
let a be object ; :: thesis: ( 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).[)) ; :: thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
per cases ( a = i or a <> i ) ;
suppose A12: a = i ; :: thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
A13: 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; :: thesis: verum
end;
suppose a <> i ; :: thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
then 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; :: thesis: 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; :: thesis: 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); :: thesis: ( e in x implies ex r being Real st
( r > 0 & Ball (e,r) c= x ) )
assume A19: e in x ; :: thesis: 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 ; :: thesis: ( r > 0 & Ball (e,r) c= x )
thus r > 0 by A23; :: thesis: Ball (e,r) c= x
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (e,r) or y in x )
assume A25: y in Ball (e,r) ; :: thesis: 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 :: thesis: 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)) . a
let a be object ; :: thesis: ( 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).[)) ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
per cases ( a = i or a <> i ) ;
suppose a = i ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a by A24, A22, A26, A28, FUNCT_7:31; :: thesis: verum
end;
suppose a <> i ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
then ( ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a & ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a = (Carrier ((Seg n) --> R^1)) . a ) by FUNCT_7:32;
hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a ; :: thesis: verum
end;
end;
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; :: thesis: 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; :: thesis: verum