src/HOL/Analysis/Conformal_Mappings.thy
 changeset 66793 deabce3ccf1f parent 66660 bc3584f7ac0c child 66827 c94531b5007d
```     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Oct 08 16:50:37 2017 +0200
1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Oct 09 15:34:23 2017 +0100
1.3 @@ -1454,6 +1454,15 @@
1.4    qed
1.5  qed
1.6
1.7 +corollary Schwarz_Lemma':
1.8 +  assumes holf: "f holomorphic_on (ball 0 1)" and [simp]: "f 0 = 0"
1.9 +      and no: "\<And>z. norm z < 1 \<Longrightarrow> norm (f z) < 1"
1.10 +    shows "((\<forall>\<xi>. norm \<xi> < 1 \<longrightarrow> norm (f \<xi>) \<le> norm \<xi>) \<and> norm(deriv f 0) \<le> 1) \<and>
1.11 +           (((\<exists>z. norm z < 1 \<and> z \<noteq> 0 \<and> norm(f z) = norm z) \<or> norm(deriv f 0) = 1)
1.12 +           \<longrightarrow> (\<exists>\<alpha>. (\<forall>z. norm z < 1 \<longrightarrow> f z = \<alpha> * z) \<and> norm \<alpha> = 1))"
1.13 +  using Schwarz_Lemma [OF assms]
1.14 +  by (metis (no_types) norm_eq_zero zero_less_one)
1.15 +
1.16  subsection\<open>The Schwarz reflection principle\<close>
1.17
1.18  lemma hol_pal_lem0:
```