equal
deleted
inserted
replaced
3372 lemma closure_outside_subset: |
3372 lemma closure_outside_subset: |
3373 fixes S :: "'a::real_normed_vector set" |
3373 fixes S :: "'a::real_normed_vector set" |
3374 assumes "closed S" |
3374 assumes "closed S" |
3375 shows "closure(outside S) \<subseteq> S \<union> outside S" |
3375 shows "closure(outside S) \<subseteq> S \<union> outside S" |
3376 by (metis assms closed_open closure_minimal inside_outside open_inside sup_ge2) |
3376 by (metis assms closed_open closure_minimal inside_outside open_inside sup_ge2) |
|
3377 |
|
3378 lemma closed_path_image_Un_inside: |
|
3379 fixes g :: "real \<Rightarrow> 'a :: real_normed_vector" |
|
3380 assumes "path g" |
|
3381 shows "closed (path_image g \<union> inside (path_image g))" |
|
3382 by (simp add: assms closed_Compl closed_path_image open_outside union_with_inside) |
3377 |
3383 |
3378 lemma frontier_outside_subset: |
3384 lemma frontier_outside_subset: |
3379 fixes S :: "'a::real_normed_vector set" |
3385 fixes S :: "'a::real_normed_vector set" |
3380 assumes "closed S" |
3386 assumes "closed S" |
3381 shows "frontier(outside S) \<subseteq> S" |
3387 shows "frontier(outside S) \<subseteq> S" |