src/HOL/Analysis/Brouwer_Fixpoint.thy

   moreover have "f a \<in> B" "g a \<in> B"
     using f g a by (auto simp: bij_betw_def)
   ultimately show ?thesis
     by auto
 qed
-
-lemma swap_image:
-  "Fun.swap i j f ` A = (if i \<in> A then (if j \<in> A then f ` A else f ` ((A - {i}) \<union> {j}))
-                                  else (if j \<in> A then f ` ((A - {j}) \<union> {i}) else f ` A))"
-  by (auto simp: swap_def cong: image_cong_simp)
 
 lemmas swap_apply1 = swap_apply(1)
 lemmas swap_apply2 = swap_apply(2)
 
 lemma pointwise_minimal_pointwise_maximal:

   show "continuous_on S f"
   unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
   using derf has_derivative_continuous by blast
 qed (use assms in auto)
 
-
 end