let E be RealNormSpace; :: thesis: for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds
Y is open
let X, Y be Subset of E; :: thesis: for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds
Y is open
let v be Point of E; :: thesis: ( X is open & Y = { (x - v) where x is Point of E : x in X } implies Y is open )
assume that
A1: X is open and
A2: Y = { (x - v) where x is Point of E : x in X } ; :: thesis: Y is open
set w = - v;
{ (x + (- v)) where x is Point of E : x in X } c= the carrier of E
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { (x + (- v)) where x is Point of E : x in X } or s in the carrier of E )
assume s in { (x + (- v)) where x is Point of E : x in X } ; :: thesis: s in the carrier of E
then ex x being Point of E st
( s = x + (- v) & x in X ) ;
hence s in the carrier of E ; :: thesis: verum
end;
then reconsider Z = { (x + (- v)) where x is Point of E : x in X } as Subset of E ;
deffunc H1( Point of E) -> Element of the carrier of E = $1 + (- v);
deffunc H2( Point of E) -> Element of the carrier of E = $1 - v;
defpred S1[ Point of E] means $1 in X;
A3: for v being Element of the carrier of E holds H1(v) = H2(v) ;
{ H1(v1) where v1 is Element of the carrier of E : S1[v1] } = { H2(v2) where v2 is Element of the carrier of E : S1[v2] } from FRAENKEL:sch 5(A3);
 hence Y is open by A1, A2, OP1; :: thesis: verum