equal
deleted
inserted
replaced
927 |
927 |
928 |
928 |
929 subsection {* Differentiability of inverse function (most basic form) *} |
929 subsection {* Differentiability of inverse function (most basic form) *} |
930 |
930 |
931 lemma has_derivative_inverse_basic: |
931 lemma has_derivative_inverse_basic: |
932 fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space" |
932 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
933 assumes "(f has_derivative f') (at (g y))" |
933 assumes "(f has_derivative f') (at (g y))" |
934 and "bounded_linear g'" |
934 and "bounded_linear g'" |
935 and "g' \<circ> f' = id" |
935 and "g' \<circ> f' = id" |
936 and "continuous (at y) g" |
936 and "continuous (at y) g" |
937 and "open t" |
937 and "open t" |
1073 qed |
1073 qed |
1074 |
1074 |
1075 text {* Simply rewrite that based on the domain point x. *} |
1075 text {* Simply rewrite that based on the domain point x. *} |
1076 |
1076 |
1077 lemma has_derivative_inverse_basic_x: |
1077 lemma has_derivative_inverse_basic_x: |
1078 fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space" |
1078 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
1079 assumes "(f has_derivative f') (at x)" |
1079 assumes "(f has_derivative f') (at x)" |
1080 and "bounded_linear g'" |
1080 and "bounded_linear g'" |
1081 and "g' \<circ> f' = id" |
1081 and "g' \<circ> f' = id" |
1082 and "continuous (at (f x)) g" |
1082 and "continuous (at (f x)) g" |
1083 and "g (f x) = x" |
1083 and "g (f x) = x" |
1091 done |
1091 done |
1092 |
1092 |
1093 text {* This is the version in Dieudonne', assuming continuity of f and g. *} |
1093 text {* This is the version in Dieudonne', assuming continuity of f and g. *} |
1094 |
1094 |
1095 lemma has_derivative_inverse_dieudonne: |
1095 lemma has_derivative_inverse_dieudonne: |
1096 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1096 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
1097 assumes "open s" |
1097 assumes "open s" |
1098 and "open (f ` s)" |
1098 and "open (f ` s)" |
1099 and "continuous_on s f" |
1099 and "continuous_on s f" |
1100 and "continuous_on (f ` s) g" |
1100 and "continuous_on (f ` s) g" |
1101 and "\<forall>x\<in>s. g (f x) = x" |
1101 and "\<forall>x\<in>s. g (f x) = x" |
1111 done |
1111 done |
1112 |
1112 |
1113 text {* Here's the simplest way of not assuming much about g. *} |
1113 text {* Here's the simplest way of not assuming much about g. *} |
1114 |
1114 |
1115 lemma has_derivative_inverse: |
1115 lemma has_derivative_inverse: |
1116 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1116 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
1117 assumes "compact s" |
1117 assumes "compact s" |
1118 and "x \<in> s" |
1118 and "x \<in> s" |
1119 and "f x \<in> interior (f ` s)" |
1119 and "f x \<in> interior (f ` s)" |
1120 and "continuous_on s f" |
1120 and "continuous_on s f" |
1121 and "\<forall>y\<in>s. g (f y) = y" |
1121 and "\<forall>y\<in>s. g (f y) = y" |