Added a couple of obvious simprules
authorpaulson <lp15@cam.ac.uk>
Thu, 05 May 2022 16:39:48 +0100
changeset 75941 51e05af57455
parent 75940 53a60eae475f
child 75944 f16d83de3e4a
Added a couple of obvious simprules
src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed May 04 07:20:20 2022 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu May 05 16:39:48 2022 +0100
@@ -19,17 +19,17 @@
   morphisms "openin" "topology"
   unfolding istopology_def by blast
 
-lemma istopology_openin[intro]: "istopology(openin U)"
+lemma istopology_openin[iff]: "istopology(openin U)"
   using openin[of U] by blast
 
-lemma istopology_open: "istopology open"
+lemma istopology_open[iff]: "istopology open"
   by (auto simp: istopology_def)
 
-lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
+lemma topology_inverse' [simp]: "istopology U \<Longrightarrow> openin (topology U) = U"
   using topology_inverse[unfolded mem_Collect_eq] .
 
 lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
-  using topology_inverse[of U] istopology_openin[of "topology U"] by auto
+  by (metis istopology_openin topology_inverse')
 
 lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
 proof