let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS m)
for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Jacobian (f,x) is invertible )
let f be PartFunc of (REAL-NS m),(REAL-NS m); :: thesis: for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Jacobian (f,x) is invertible )
let x be Point of (REAL-NS m); :: thesis: ( f is_differentiable_in x implies ( diff (f,x) is invertible iff Jacobian (f,x) is invertible ) )
assume f is_differentiable_in x ; :: thesis: ( diff (f,x) is invertible iff Jacobian (f,x) is invertible )
then diff (f,x) = Mx2Tran (Jacobian (f,x)) by Th29;
hence ( diff (f,x) is invertible iff Jacobian (f,x) is invertible ) by Th12; :: thesis: verum