equal
deleted
inserted
replaced
1 (* Title: HOL/Analysis/Arcwise_Connected.thy |
1 (* Title: HOL/Analysis/Arcwise_Connected.thy |
2 Authors: LC Paulson, based on material from HOL Light |
2 Authors: LC Paulson, based on material from HOL Light |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Arcwise-connected sets\<close> |
5 section \<open>Arcwise-Connected Sets\<close> |
6 |
6 |
7 theory Arcwise_Connected |
7 theory Arcwise_Connected |
8 imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes" |
8 imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes" |
9 |
|
10 begin |
9 begin |
11 |
10 |
12 subsection%important \<open>The Brouwer reduction theorem\<close> |
11 subsection%important \<open>The Brouwer reduction theorem\<close> |
13 |
12 |
14 theorem%important Brouwer_reduction_theorem_gen: |
13 theorem%important Brouwer_reduction_theorem_gen: |