Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Abstract_Topology.thy
changeset 78200 264f2b69d09c
parent 78127 24b70433c2e8
child 78248 740b23f1138a 
--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Jun 23 14:43:15 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jun 26 14:38:19 2023 +0100
@@ -3033,7 +3033,7 @@
 definition homeomorphic_space (infixr "homeomorphic'_space" 50)
   where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
 
-lemma homeomorphic_space_refl: "X homeomorphic_space X"
+lemma homeomorphic_space_refl [iff]: "X homeomorphic_space X"
   by (meson homeomorphic_maps_id homeomorphic_space_def)
 
 lemma homeomorphic_space_sym:
isabelle