src/HOL/Orderings.thy
changeset 64287 d85d88722745
parent 63819 58f74e90b96d
child 64758 3b33d2fc5fc0
     1.1 --- a/src/HOL/Orderings.thy	Tue Oct 18 12:01:54 2016 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Oct 18 15:55:53 2016 +0100
     1.3 @@ -1437,6 +1437,17 @@
     1.4  apply (erule Least_le)
     1.5  done
     1.6  
     1.7 +lemma exists_least_iff: "(\<exists>n. P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" (is "?lhs \<longleftrightarrow> ?rhs")
     1.8 +proof
     1.9 +  assume ?rhs thus ?lhs by blast
    1.10 +next
    1.11 +  assume H: ?lhs then obtain n where n: "P n" by blast
    1.12 +  let ?x = "Least P"
    1.13 +  { fix m assume m: "m < ?x"
    1.14 +    from not_less_Least[OF m] have "\<not> P m" . }
    1.15 +  with LeastI_ex[OF H] show ?rhs by blast
    1.16 +qed
    1.17 +
    1.18  end
    1.19  
    1.20