author | paulson <lp15@cam.ac.uk> |
Sun, 19 Apr 2020 22:58:32 +0100 | |
changeset 71772 | af1381b565d6 |
parent 71771 | 7c0de1eb6075 |
child 71773 | 7c2f4dd48fb6 |
--- a/src/HOL/Analysis/Further_Topology.thy Sun Apr 19 22:16:57 2020 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Sun Apr 19 22:58:32 2020 +0100 @@ -4,7 +4,6 @@ theory Further_Topology imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts -Sketch_and_Explore begin subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>