let n be non zero Element of NAT ; :: thesis: for Y being Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open
let Y be Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on Y holds
Y is open
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; :: thesis: Y is open
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A2: Y c= dom g by A1;
now :: thesis: for x being Real st x in Y holds
g | Y is_differentiable_in x
let x be Real; :: thesis: ( x in Y implies g | Y is_differentiable_in x )
assume x in Y ; :: thesis: g | Y is_differentiable_in x
then f | Y is_differentiable_in x by A1;
hence g | Y is_differentiable_in x ; :: thesis: verum
end;
then g is_differentiable_on Y by A2, NDIFF_3:def 5;
hence Y is open by NDIFF_3:11; :: thesis: verum