src/HOL/Library/Indicator_Function.thy
changeset 69313 b021008c5397
parent 67683 817944aeac3f
     1.1 --- a/src/HOL/Library/Indicator_Function.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Indicator_Function.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -191,7 +191,7 @@
     1.4  \<close>
     1.5  
     1.6  lemma indicator_UN_disjoint:
     1.7 -  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
     1.8 +  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
     1.9    by (induct A rule: finite_induct)
    1.10      (auto simp: disjoint_family_on_def indicator_def split: if_splits)
    1.11