src/HOL/Analysis/Riemann_Mapping.thy
changeset 67968 a5ad4c015d1c
parent 67685 bdff8bf0a75b
child 68634 db0980691ef4
     1.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Apr 09 16:20:23 2018 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Great_Picard
     1.5  begin
     1.6  
     1.7 -subsection\<open>Moebius functions are biholomorphisms of the unit disc.\<close>
     1.8 +subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
     1.9  
    1.10  definition Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
    1.11    "Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
    1.12 @@ -853,7 +853,7 @@
    1.13    using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
    1.14  
    1.15  
    1.16 -subsection\<open>A further chain of equivalences about components of the complement of a simply connected set.\<close>
    1.17 +subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
    1.18  
    1.19  text\<open>(following 1.35 in Burckel'S book)\<close>
    1.20