author nipkow Wed Dec 04 12:00:07 2019 +0100 (2 days ago ago) changeset 71428 1249859d23dd parent 71427 54a7ad860a76 child 71429 dc767054de47 child 71431 e9a4bd0a836e
moved lemma
```     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Dec 03 16:51:53 2019 +0100
1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 04 12:00:07 2019 +0100
1.3 @@ -455,6 +455,11 @@
1.4    shows "closure S \<subseteq> affine hull S"
1.5    by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
1.6
1.7 +lemma closed_affine_hull [iff]:
1.8 +  fixes S :: "'n::euclidean_space set"
1.9 +  shows "closed (affine hull S)"
1.10 +  by (metis affine_affine_hull affine_closed)
1.11 +
1.12  lemma closure_same_affine_hull [simp]:
1.13    fixes S :: "'n::euclidean_space set"
1.14    shows "affine hull (closure S) = affine hull S"
```
```     2.1 --- a/src/HOL/Analysis/Starlike.thy	Tue Dec 03 16:51:53 2019 +0100
2.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:00:07 2019 +0100
2.3 @@ -1296,11 +1296,6 @@
2.4    shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)"
2.5  by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)
2.6
2.7 -lemma closed_affine_hull [iff]:
2.8 -  fixes S :: "'n::euclidean_space set"
2.9 -  shows "closed (affine hull S)"
2.10 -  by (metis affine_affine_hull affine_closed)
2.11 -
2.12  lemma rel_frontier_nonempty_interior:
2.13    fixes S :: "'n::euclidean_space set"
2.14    shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S"
```