# HG changeset patch # User nipkow # Date 1574969887 -3600 # Node ID a25b6f79043f29a93f050e76f99dde01881ea995 # Parent df1d96114754df10f6169983e9852b6b412923c0# Parent 57bc95d2349106659892a04a617bfe6a445069e1 merged diff -r 57bc95d23491 -r a25b6f79043f src/HOL/Analysis/Line_Segment.thy --- a/src/HOL/Analysis/Line_Segment.thy Thu Nov 28 18:40:39 2019 +0100 +++ b/src/HOL/Analysis/Line_Segment.thy Thu Nov 28 20:38:07 2019 +0100 @@ -14,7 +14,7 @@ Topology_Euclidean_Space begin -subsection\<^marker>\tag unimportant\ \Topological Properties of Convex Sets and Functions\ +subsection\<^marker>\tag unimportant\ \Topological Properties of Convex Sets, Metric Spaces and Functions\ lemma convex_supp_sum: assumes "convex S" and 1: "supp_sum u I = 1" @@ -23,13 +23,11 @@ proof - have fin: "finite {i \ I. u i \ 0}" using 1 sum.infinite by (force simp: supp_sum_def support_on_def) - then have eq: "supp_sum (\i. u i *\<^sub>R f i) I = sum (\i. u i *\<^sub>R f i) {i \ I. u i \ 0}" + then have "supp_sum (\i. u i *\<^sub>R f i) I = sum (\i. u i *\<^sub>R f i) {i \ I. u i \ 0}" by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) - show ?thesis - apply (simp add: eq) - apply (rule convex_sum [OF fin \convex S\]) - using 1 assms apply (auto simp: supp_sum_def support_on_def) - done + also have "... \ S" + using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \convex S\]) + finally show ?thesis . qed lemma closure_bounded_linear_image_subset: @@ -135,7 +133,7 @@ proposition clopen: fixes S :: "'a :: real_normed_vector set" shows "closed S \ open S \ S = {} \ S = UNIV" - by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) + by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) corollary compact_open: fixes S :: "'a :: euclidean_space set" @@ -143,8 +141,8 @@ by (auto simp: compact_eq_bounded_closed clopen) corollary finite_imp_not_open: - fixes S :: "'a::{real_normed_vector, perfect_space} set" - shows "\finite S; open S\ \ S={}" + fixes S :: "'a::{real_normed_vector, perfect_space} set" + shows "\finite S; open S\ \ S={}" using clopen [of S] finite_imp_closed not_bounded_UNIV by blast corollary empty_interior_finite: @@ -246,11 +244,7 @@ from assms obtain B where B: "\x\s. norm x \ B" unfolding bounded_iff by auto show ?thesis - apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) - unfolding subset_hull[of convex, OF convex_cball] - unfolding subset_eq mem_cball dist_norm using B - apply auto - done + by (simp add: bounded_subset[OF bounded_cball, of _ 0 B] B subsetI subset_hull) qed lemma finite_imp_bounded_convex_hull: @@ -260,8 +254,6 @@ by auto -section \Line Segments\ - subsection \Midpoint\ definition\<^marker>\tag important\ midpoint :: "'a::real_vector \ 'a \ 'a" @@ -338,7 +330,7 @@ by (simp add: linear_iff midpoint_def) -subsection \Line segments\ +subsection \Open and closed segments\ definition\<^marker>\tag important\ closed_segment :: "'a::real_vector \ 'a \ 'a set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" @@ -528,8 +520,7 @@ lemma segment_bound: assumes "x \ closed_segment a b" shows "norm (x - a) \ norm (b - a)" "norm (x - b) \ norm (b - a)" -apply (simp add: assms segment_bound1) -by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) +by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+ lemma open_segment_commute: "open_segment a b = open_segment b a" proof - @@ -564,8 +555,11 @@ by (auto intro!: mult_left_mono u assms) then show "x \ {a .. b}" unfolding x_def by (auto simp: algebra_simps) -qed (auto simp: closed_segment_def divide_simps algebra_simps - intro!: exI[where x="(x - a) / (b - a)" for x]) +next + show "\x. x \ {a..b} \ x \ closed_segment a b" + by (force simp: closed_segment_def divide_simps algebra_simps + intro: exI[where x="(x - a) / (b - a)" for x]) +qed lemma closed_segment_eq_real_ivl: fixes a b::real