src/HOL/Set.thy
changeset 11982 65e2822d83dd
parent 11979 0a3dace545c5
child 12020 a24373086908
     1.1 --- a/src/HOL/Set.thy	Mon Oct 29 17:22:18 2001 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Oct 30 13:43:26 2001 +0100
     1.3 @@ -893,4 +893,15 @@
     1.4  use "equalities.ML"
     1.5  use "mono.ML"
     1.6  
     1.7 +lemma Least_mono:
     1.8 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     1.9 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    1.10 +    -- {* Courtesy of Stephan Merz *}
    1.11 +  apply clarify
    1.12 +  apply (erule_tac P = "%x. x : S" in LeastI2)
    1.13 +   apply fast
    1.14 +  apply (rule LeastI2)
    1.15 +  apply (auto elim: monoD intro!: order_antisym)
    1.16 +  done
    1.17 +
    1.18  end