let X be LinearTopSpace; :: thesis: for U, V being a_neighborhood of 0. X
for F being Subset-Family of X
for r being positive Real st ( for s being Real st |.s.| < r holds
s * V c= U ) & F = { (a * V) where a is Real : |.a.| < r } holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let U, V be a_neighborhood of 0. X; :: thesis: for F being Subset-Family of X
for r being positive Real st ( for s being Real st |.s.| < r holds
s * V c= U ) & F = { (a * V) where a is Real : |.a.| < r } holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let F be Subset-Family of X; :: thesis: for r being positive Real st ( for s being Real st |.s.| < r holds
s * V c= U ) & F = { (a * V) where a is Real : |.a.| < r } holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let r be positive Real; :: thesis: ( ( for s being Real st |.s.| < r holds
s * V c= U ) & F = { (a * V) where a is Real : |.a.| < r } implies ( union F is a_neighborhood of 0. X & union F is circled & union F c= U ) )
assume that
A1: for s being Real st |.s.| < r holds
s * V c= U and
A2: F = { (a * V) where a is Real : |.a.| < r } ; :: thesis: ( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
set W = union F;
thus union F is a_neighborhood of 0. X :: thesis: ( union F is circled & union F c= U )
proof
set F9 = { (a * (Int V)) where a is non zero Real : |.a.| < r } ;
consider a being Real such that
A3: 0 < a and
A4: a < r by XREAL_1:5;
reconsider a = a as Real ;
0. X in Int V by CONNSP_2:def 1;
then a * (0. X) in a * (Int V) ;
then A5: 0. X in a * (Int V) ;
A6: { (a * (Int V)) where a is non zero Real : |.a.| < r } c= bool the carrier of X
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { (a * (Int V)) where a is non zero Real : |.a.| < r } or A in bool the carrier of X )
assume A in { (a * (Int V)) where a is non zero Real : |.a.| < r } ; :: thesis: A in bool the carrier of X
then ex a being non zero Real st
( A = a * (Int V) & |.a.| < r ) ;
hence A in bool the carrier of X ; :: thesis: verum
end;
|.a.| < r by A3, A4, ABSVALUE:def 1;
then a * (Int V) in { (a * (Int V)) where a is non zero Real : |.a.| < r } by A3;
then A7: 0. X in union { (a * (Int V)) where a is non zero Real : |.a.| < r } by A5, TARSKI:def 4;
reconsider F9 = { (a * (Int V)) where a is non zero Real : |.a.| < r } as Subset-Family of X by A6;
union F9 c= union F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F9 or x in union F )
A8: Int V c= V by TOPS_1:16;
assume x in union F9 ; :: thesis: x in union F
then consider P being set such that
A9: x in P and
A10: P in F9 by TARSKI:def 4;
consider a being non zero Real such that
A11: P = a * (Int V) and
A12: |.a.| < r by A10;
ex v being Point of X st
( x = a * v & v in Int V ) by A9, A11;
then A13: x in a * V by A8;
a * V in F by A2, A12;
hence x in union F by A13, TARSKI:def 4; :: thesis: verum
end;
then A14: Int (union F9) c= Int (union F) by TOPS_1:19;
F9 is open
proof
let P be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not P in F9 or P is open )
assume P in F9 ; :: thesis: P is open
then ex a being non zero Real st
( P = a * (Int V) & |.a.| < r ) ;
hence P is open by Th49; :: thesis: verum
end;
then union F9 is open by TOPS_2:19;
then 0. X in Int (union F9) by A7, TOPS_1:23;
hence 0. X in Int (union F) by A14; :: according to CONNSP_2:def 1 :: thesis: verum
end;
thus union F is circled :: thesis: union F c= U
proof
let s be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.s.| <= 1 implies s * (union F) c= union F )
assume |.s.| <= 1 ; :: thesis: s * (union F) c= union F
then A15: |.s.| * r <= r by XREAL_1:153;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in s * (union F) or z in union F )
assume z in s * (union F) ; :: thesis: z in union F
then consider u being Point of X such that
A16: z = s * u and
A17: u in union F ;
consider Y being set such that
A18: u in Y and
A19: Y in F by A17, TARSKI:def 4;
consider a being Real such that
A20: Y = a * V and
A21: |.a.| < r by A2, A19;
consider v being Point of X such that
A22: u = a * v and
A23: v in V by A18, A20;
z = (s * a) * v by A16, A22, RLVECT_1:def 7;
then A24: z in (s * a) * V by A23;
per cases ( 0 <> |.s.| or |.s.| = 0 ) ;
end;
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union F or z in U )
assume A25: z in union F ; :: thesis: z in U
then reconsider z = z as Point of X ;
consider Y being set such that
A26: z in Y and
A27: Y in F by A25, TARSKI:def 4;
consider a being Real such that
A28: Y = a * V and
A29: |.a.| < r by A2, A27;
a * V c= U by A1, A29;
hence z in U by A26, A28; :: thesis: verum