equal
deleted
inserted
replaced
6 Author: Johannes Hoelzl, TU Muenchen |
6 Author: Johannes Hoelzl, TU Muenchen |
7 *) |
7 *) |
8 chapter \<open>Unsorted\<close> |
8 chapter \<open>Unsorted\<close> |
9 |
9 |
10 theory Starlike |
10 theory Starlike |
11 imports Convex_Euclidean_Space Abstract_Limits |
11 imports |
|
12 Convex_Euclidean_Space |
|
13 Abstract_Limits |
|
14 Line_Segment |
12 begin |
15 begin |
13 |
16 |
14 subsection\<open>Starlike sets\<close> |
17 subsection\<open>Starlike sets\<close> |
15 |
18 |
16 definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)" |
19 definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)" |