# HG changeset patch
# User nipkow
# Date 1612810125 -3600
# Node ID b1aa641eee4c529497de1b43203903fa5793bed1
# Parent  6974bca47856ff64581b244ab710592ab4949ebd
added lemmas

diff -r 6974bca47856 -r b1aa641eee4c src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Feb 01 16:03:07 2021 +0100
+++ b/src/HOL/Lattices_Big.thy	Mon Feb 08 19:48:45 2021 +0100
@@ -560,6 +560,12 @@
   ultimately show ?thesis by (simp add: max.absorb1)
 qed
 
+lemma Max_const[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max ((\<lambda>_. c) ` A) = c"
+using Max_in image_is_empty by blast
+
+lemma Min_const[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min ((\<lambda>_. c) ` A) = c"
+using Min_in image_is_empty by blast
+
 lemma Min_le [simp]:
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
@@ -671,6 +677,12 @@
 
 end
 
+lemma sum_le_card_Max: "finite A \<Longrightarrow> sum f A \<le> card A * Max (f ` A)"
+using sum_bounded_above[of A f "Max (f ` A)"] by simp
+
+lemma card_Min_le_sum: "finite A \<Longrightarrow> card A * Min (f ` A) \<le> sum f A"
+using sum_bounded_below[of A "Min (f ` A)" f] by simp
+
 context linorder  (* FIXME *)
 begin