let E be RealNormSpace; :: thesis: for x, b being Point of E
for N being Neighbourhood of x holds
( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )
let x, b be Point of E; :: thesis: for N being Neighbourhood of x holds
( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )
let N be Neighbourhood of x; :: thesis: ( { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b & { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b )
consider g being Real such that
A1: ( 0 < g & { y where y is Point of E : ||.(y - x).|| < g } c= N ) by NFCONT_1:def 1;
set V = { y where y is Point of E : ||.(y - x).|| < g } ;
B2: { (z - b) where z is Point of E : z in N } c= the carrier of E
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { (z - b) where z is Point of E : z in N } or s in the carrier of E )
assume s in { (z - b) where z is Point of E : z in N } ; :: thesis: s in the carrier of E
then ex z being Point of E st
( s = z - b & z in N ) ;
hence s in the carrier of E ; :: thesis: verum
end;
B3: { (z + b) where z is Point of E : z in N } c= the carrier of E
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { (z + b) where z is Point of E : z in N } or s in the carrier of E )
assume s in { (z + b) where z is Point of E : z in N } ; :: thesis: s in the carrier of E
then ex z being Point of E st
( s = z + b & z in N ) ;
hence s in the carrier of E ; :: thesis: verum
end;
{ y where y is Point of E : ||.(y - (x - b)).|| < g } c= { (z - b) where z is Point of E : z in N }
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Point of E : ||.(y - (x - b)).|| < g } or t in { (z - b) where z is Point of E : z in N } )
assume t in { y where y is Point of E : ||.(y - (x - b)).|| < g } ; :: thesis: t in { (z - b) where z is Point of E : z in N }
then consider y being Point of E such that
A4: ( t = y & ||.(y - (x - b)).|| < g ) ;
y - (x - b) = (y - x) + b by RLVECT_1:29
.= (y + b) - x by RLVECT_1:def 3 ;
then A5: y + b in { y where y is Point of E : ||.(y - x).|| < g } by A4;
y = (y + b) - b by RLVECT_4:1;
hence t in { (z - b) where z is Point of E : z in N } by A1, A4, A5; :: thesis: verum
end;
hence { (z - b) where z is Point of E : z in N } is Neighbourhood of x - b by A1, B2, NFCONT_1:def 1; :: thesis: { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b
{ y where y is Point of E : ||.(y - (x + b)).|| < g } c= { (z + b) where z is Point of E : z in N }
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Point of E : ||.(y - (x + b)).|| < g } or t in { (z + b) where z is Point of E : z in N } )
assume t in { y where y is Point of E : ||.(y - (x + b)).|| < g } ; :: thesis: t in { (z + b) where z is Point of E : z in N }
then consider y being Point of E such that
A6: ( t = y & ||.(y - (x + b)).|| < g ) ;
||.((y - b) - x).|| < g by A6, RLVECT_1:27;
then A7: y - b in { y where y is Point of E : ||.(y - x).|| < g } ;
y = (y - b) + b by RLVECT_4:1;
hence t in { (z + b) where z is Point of E : z in N } by A1, A6, A7; :: thesis: verum
end;
hence { (z + b) where z is Point of E : z in N } is Neighbourhood of x + b by A1, B3, NFCONT_1:def 1; :: thesis: verum