src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 67399 eab6ce8368fa
parent 66939 04678058308f
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4      by (subst card_Un_disjoint[symmetric])
     1.5         (auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
     1.6    also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
     1.7 -    using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] sum_multicount)
     1.8 +    using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
     1.9    finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
    1.10      using assms(6,8) by simp
    1.11    moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
    1.12 @@ -4221,13 +4221,13 @@
    1.13          show "ANR (C \<inter> \<Union>\<U>)"
    1.14            unfolding Int_Union
    1.15          proof (rule Suc)
    1.16 -          show "finite (op \<inter> C ` \<U>)"
    1.17 +          show "finite ((\<inter>) C ` \<U>)"
    1.18              by (simp add: insert.hyps(1))
    1.19 -          show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> closed Ca"
    1.20 +          show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> closed Ca"
    1.21              by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2)
    1.22 -          show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> convex Ca"
    1.23 +          show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> convex Ca"
    1.24              by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE)
    1.25 -          show "card (op \<inter> C ` \<U>) < n"
    1.26 +          show "card ((\<inter>) C ` \<U>) < n"
    1.27            proof -
    1.28              have "card \<T> \<le> n"
    1.29                by (meson Suc.prems(4) not_less not_less_eq)