equal
deleted
inserted
replaced
126 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
126 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
127 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
127 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
128 using assms[simp] |
128 using assms[simp] |
129 proof - |
129 proof - |
130 have "?L = Max (\<Union>(f ` A))" |
130 have "?L = Max (\<Union>(f ` A))" |
131 by (fold Union_image_eq, simp) |
131 by simp |
132 also have "... = ?R" |
132 also have "... = ?R" |
133 by (subst Max_Union, simp+) |
133 by (subst Max_Union, simp+) |
134 finally show ?thesis . |
134 finally show ?thesis |
|
135 using \<open>Max (UNION A f) = Max (Max ` f ` A)\<close> by blast |
135 qed |
136 qed |
136 |
137 |
137 lemma max_Max_eq: |
138 lemma max_Max_eq: |
138 assumes "finite A" |
139 assumes "finite A" |
139 and "A \<noteq> {}" |
140 and "A \<noteq> {}" |