# HG changeset patch # User huffman # Date 1272337131 25200 # Node ID d8b26fac82f5281b2f5e537045694c93398e220d # Parent e76cb1d4663c5207b981e686c6f45a969274b9d9 remove unused, redundant constant inv_on diff -r e76cb1d4663c -r d8b26fac82f5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 26 19:55:50 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 26 19:58:51 2010 -0700 @@ -5329,12 +5329,6 @@ text {* Relatively weak hypotheses if a set is compact. *} -definition "inv_on f s = (\x. SOME y. y\s \ f y = x)" - -lemma assumes "inj_on f s" "x\s" - shows "inv_on f s (f x) = x" - using assms unfolding inj_on_def inv_on_def by auto - lemma homeomorphism_compact: fixes f :: "'a::heine_borel \ 'b::heine_borel" (* class constraint due to continuous_on_inverse *)