--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Mar 22 10:49:51 2021 +0000
@@ -234,11 +234,6 @@
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)
@@ -2598,5 +2593,4 @@
using derf has_derivative_continuous by blast
qed (use assms in auto)
-
end