# HG changeset patch # User haftmann # Date 1614112908 0 # Node ID 6c4c37a3ebec0d763eb8317952e95f5c097a9ae7 # Parent f0210642e43fa0c1db0ca5e11db3c9a0522981fb dropped obscure FIXME diff -r f0210642e43f -r 6c4c37a3ebec src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Tue Feb 23 12:20:50 2021 +0100 +++ b/src/HOL/Lattices_Big.thy Tue Feb 23 20:41:48 2021 +0000 @@ -675,17 +675,6 @@ shows "Max M \ Max N" using assms by (fact Max.subset_imp) -end - -lemma sum_le_card_Max: "finite A \ sum f A \ card A * Max (f ` A)" -using sum_bounded_above[of A f "Max (f ` A)"] by simp - -lemma card_Min_le_sum: "finite A \ card A * Min (f ` A) \ sum f A" -using sum_bounded_below[of A "Min (f ` A)" f] by simp - -context linorder (* FIXME *) -begin - lemma mono_Min_commute: assumes "mono f" assumes "finite A" and "A \ {}" @@ -810,6 +799,12 @@ end +lemma sum_le_card_Max: "finite A \ sum f A \ card A * Max (f ` A)" +using sum_bounded_above[of A f "Max (f ` A)"] by simp + +lemma card_Min_le_sum: "finite A \ card A * Min (f ` A) \ sum f A" +using sum_bounded_below[of A "Min (f ` A)" f] by simp + context linordered_ab_semigroup_add begin