Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalized
authorimmler
Mon, 29 Feb 2016 16:35:15 +0100
changeset 62466 87ca8b5145b8
parent 62465 2e4c6ef809b5
child 62476 d396da07055d
generalized
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 15:14:45 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 29 16:35:15 2016 +0100
@@ -3437,7 +3437,7 @@
 qed
 
 lemma bounded_uminus [simp]:
-  fixes X :: "'a::euclidean_space set"
+  fixes X :: "'a::real_normed_vector set"
   shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
isabelle