let F be RealNormSpace; :: thesis: for Y being Subset of REAL
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
let Y be Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on Y holds
Y is open
let f be PartFunc of REAL, the carrier of F; :: thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; :: thesis: Y is open
now :: thesis: for x0 being Element of REAL st x0 in Y holds
ex N being Neighbourhood of x0 st N c= Y
let x0 be Element of REAL ; :: thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )
assume x0 in Y ; :: thesis: ex N being Neighbourhood of x0 st N c= Y
then f | Y is_differentiable_in x0 by A1;
then consider N being Neighbourhood of x0 such that
A2: N c= dom (f | Y) and
ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
((f | Y) /. x) - ((f | Y) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
take N = N; :: thesis: N c= Y
thus N c= Y by A2, XBOOLE_1:1; :: thesis: verum
end;
hence Y is open by RCOMP_1:20; :: thesis: verum