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;

hence Y is open by NDIFF_3:11; :: thesis: verum

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

then
g is_differentiable_on Y
by A2, NDIFF_3:def 5;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;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

hence Y is open by NDIFF_3:11; :: thesis: verum