# HG changeset patch
# User nipkow
# Date 1517568433 -3600
# Node ID c555f1778dd8f6cda4c0b31bebcbe1cc8c98746a
# Parent  e13378b304dda31ad80cf86c94fd17c7ef959469
added lemma

diff -r e13378b304dd -r c555f1778dd8 src/HOL/Lattices_Big.thy
--- 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;