src/HOL/Analysis/Fashoda_Theorem.thy

 
 theory Fashoda_Theorem
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
 begin
 
-subsection%important \<open>Bijections between intervals\<close>
+subsection \<open>Bijections between intervals\<close>
 
 definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
   where "interval_bij =
     (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
 

 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
   shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
   using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
 
 
-subsection%important \<open>Fashoda meet theorem\<close>
+subsection \<open>Fashoda meet theorem\<close>
 
 lemma infnorm_2:
   fixes x :: "real^2"
   shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
   unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto

     qed
   }
 qed
 
 
-subsection%important \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
+subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
 
 corollary fashoda_interlace:
   fixes a :: "real^2"
   assumes "path f"
     and "path g"