author paulson Sat, 02 Nov 2019 18:47:00 +0000 changeset 71002 9d0712c74834 parent 71001 3e374c65f96b child 71003 699ff83813c0 child 71004 b86d30707837
oops — fixed symbols!!
```--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sat Nov 02 15:52:47 2019 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sat Nov 02 18:47:00 2019 +0000
@@ -1271,30 +1271,20 @@
text\<open>Hence a nice clean inverse function theorem\<close>

lemma has_field_derivative_inverse_strong:
-  fixes f :: "'a::{euclidean_space,real_normed_field} ⇒ 'a"
-  shows "DERIV f x :> f' ⟹
-         f' ≠ 0 ⟹
-         open S ⟹
-         x ∈ S ⟹
-         continuous_on S f ⟹
-         (⋀z. z ∈ S ⟹ g (f z) = z)
-         ⟹ DERIV g (f x) :> inverse (f')"
+  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
+  shows "\<lbrakk>DERIV f x :> f'; f' \<noteq> 0; open S; x \<in> S; continuous_on S f;
+         \<And>z. z \<in> S \<Longrightarrow> g (f z) = z\<rbrakk>
+         \<Longrightarrow> DERIV g (f x) :> inverse (f')"
unfolding has_field_derivative_def
-  apply (rule has_derivative_inverse_strong [of S x f g ])
-  by auto
+  by (rule has_derivative_inverse_strong [of S x f g]) auto

lemma has_field_derivative_inverse_strong_x:
-  fixes f :: "'a::{euclidean_space,real_normed_field} ⇒ 'a"
-  shows  "DERIV f (g y) :> f' ⟹
-          f' ≠ 0 ⟹
-          open S ⟹
-          continuous_on S f ⟹
-          g y ∈ S ⟹ f(g y) = y ⟹
-          (⋀z. z ∈ S ⟹ g (f z) = z)
-          ⟹ DERIV g y :> inverse (f')"
+  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
+  shows  "\<lbrakk>DERIV f (g y) :> f'; f' \<noteq> 0; open S; continuous_on S f; g y \<in> S; f(g y) = y;
+           \<And>z. z \<in> S \<Longrightarrow> g (f z) = z\<rbrakk>
+          \<Longrightarrow> DERIV g y :> inverse (f')"
unfolding has_field_derivative_def
-  apply (rule has_derivative_inverse_strong_x [of S g y f])
-  by auto
+  by (rule has_derivative_inverse_strong_x [of S g y f]) auto

proposition holomorphic_has_inverse:
assumes holf: "f holomorphic_on S"```