--- a/src/HOL/Lattices_Big.thy Thu Feb 01 20:29:53 2018 +0100
+++ b/src/HOL/Lattices_Big.thy Fri Feb 02 11:47:13 2018 +0100
@@ -845,6 +845,10 @@
shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))"
by(auto simp add: is_arg_min_def)
+lemma is_arg_min_antimono: fixes f :: "'a \<Rightarrow> ('b::order)"
+shows "\<lbrakk> is_arg_min f P x; f y \<le> f x; P y \<rbrakk> \<Longrightarrow> is_arg_min f P y"
+by (simp add: order.order_iff_strict is_arg_min_def)
+
lemma arg_minI:
"\<lbrakk> P x;
\<And>y. P y \<Longrightarrow> \<not> f y < f x;