equal
deleted
inserted
replaced
3 Author: Robert Himmelmann, TU Muenchen |
3 Author: Robert Himmelmann, TU Muenchen |
4 Author: Bogdan Grechuk, University of Edinburgh |
4 Author: Bogdan Grechuk, University of Edinburgh |
5 Author: Armin Heller, TU Muenchen |
5 Author: Armin Heller, TU Muenchen |
6 Author: Johannes Hoelzl, TU Muenchen |
6 Author: Johannes Hoelzl, TU Muenchen |
7 *) |
7 *) |
8 |
8 chapter \<open>Unsorted\<close> |
9 section \<open>Line Segments\<close> |
|
10 |
9 |
11 theory Starlike |
10 theory Starlike |
12 imports Convex_Euclidean_Space |
11 imports Convex_Euclidean_Space |
13 begin |
12 begin |
|
13 |
|
14 section \<open>Line Segments\<close> |
14 |
15 |
15 subsection \<open>Midpoint\<close> |
16 subsection \<open>Midpoint\<close> |
16 |
17 |
17 definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
18 definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a" |
18 where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |
19 where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" |