equal
deleted
inserted
replaced
1974 lemma Least_mono: |
1974 lemma Least_mono: |
1975 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
1975 "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y |
1976 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
1976 ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" |
1977 -- {* Courtesy of Stephan Merz *} |
1977 -- {* Courtesy of Stephan Merz *} |
1978 apply clarify |
1978 apply clarify |
1979 apply (erule_tac P = "%x. x : S" in LeastI2, fast) |
1979 apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) |
1980 apply (rule LeastI2) |
1980 apply (rule LeastI2_order) |
1981 apply (auto elim: monoD intro!: order_antisym) |
1981 apply (auto elim: monoD intro!: order_antisym) |
1982 done |
1982 done |
1983 |
1983 |
1984 |
1984 |
1985 subsection {* Inverse image of a function *} |
1985 subsection {* Inverse image of a function *} |