src/HOL/Analysis/Homotopy.thy
changeset 69712 dc85b5b3a532
parent 69620 19d8a59481db
child 69768 7e4966eaf781
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 10:50:47 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 12:00:16 2019 +0000
     1.3 @@ -2470,7 +2470,7 @@
     1.4      then have *: "openin ?SS (F y t) \<and> path_connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t"
     1.5        using 1 \<open>y \<in> t\<close> by presburger
     1.6      have "G y t \<subseteq> path_component_set t y"
     1.7 -      using * path_component_maximal set_rev_mp by blast
     1.8 +      using * path_component_maximal rev_subsetD by blast
     1.9      then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x"
    1.10        by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y)
    1.11    }