src/HOL/Multivariate_Analysis/Path_Connected.thy
changeset 44170 510ac30f44c0
parent 41959 b460124855b8
child 44531 1d477a2b1572
     1.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -387,16 +387,14 @@
     1.4  
     1.5  subsection {* Can also consider it as a set, as the name suggests. *}
     1.6  
     1.7 -lemma path_component_set: "path_component s x = { y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y )}"
     1.8 -  apply(rule set_eqI) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto
     1.9 -
    1.10 -lemma mem_path_component_set:"x \<in> path_component s y \<longleftrightarrow> path_component s y x" unfolding mem_def by auto
    1.11 +lemma path_component_set: "{y. path_component s x y} = { y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y )}"
    1.12 +  apply(rule set_eqI) unfolding mem_Collect_eq unfolding path_component_def by auto
    1.13  
    1.14 -lemma path_component_subset: "(path_component s x) \<subseteq> s"
    1.15 -  apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def)
    1.16 +lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
    1.17 +  apply(rule, rule path_component_mem(2)) by auto
    1.18  
    1.19 -lemma path_component_eq_empty: "path_component s x = {} \<longleftrightarrow> x \<notin> s"
    1.20 -  apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_path_component_set
    1.21 +lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
    1.22 +  apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_Collect_eq
    1.23    apply(drule path_component_mem(1)) using path_component_refl by auto
    1.24  
    1.25  subsection {* Path connectedness of a space. *}
    1.26 @@ -406,9 +404,9 @@
    1.27  lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
    1.28    unfolding path_connected_def path_component_def by auto
    1.29  
    1.30 -lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component s x = s)" 
    1.31 +lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" 
    1.32    unfolding path_connected_component apply(rule, rule, rule, rule path_component_subset) 
    1.33 -  unfolding subset_eq mem_path_component_set Ball_def mem_def by auto
    1.34 +  unfolding subset_eq mem_Collect_eq Ball_def by auto
    1.35  
    1.36  subsection {* Some useful lemmas about path-connectedness. *}
    1.37  
    1.38 @@ -435,25 +433,25 @@
    1.39  
    1.40  lemma open_path_component:
    1.41    fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
    1.42 -  assumes "open s" shows "open(path_component s x)"
    1.43 +  assumes "open s" shows "open {y. path_component s x y}"
    1.44    unfolding open_contains_ball proof
    1.45 -  fix y assume as:"y \<in> path_component s x"
    1.46 -  hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto
    1.47 +  fix y assume as:"y \<in> {y. path_component s x y}"
    1.48 +  hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_Collect_eq by auto
    1.49    then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
    1.50 -  show "\<exists>e>0. ball y e \<subseteq> path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_path_component_set proof-
    1.51 +  show "\<exists>e>0. ball y e \<subseteq> {y. path_component s x y}" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_Collect_eq proof-
    1.52      fix z assume "dist y z < e" thus "path_component s x z" apply(rule_tac path_component_trans[of _ _ y]) defer 
    1.53        apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0`
    1.54 -      using as[unfolded mem_def] by auto qed qed
    1.55 +      using as by auto qed qed
    1.56  
    1.57  lemma open_non_path_component:
    1.58    fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
    1.59 -  assumes "open s" shows "open(s - path_component s x)"
    1.60 +  assumes "open s" shows "open(s - {y. path_component s x y})"
    1.61    unfolding open_contains_ball proof
    1.62 -  fix y assume as:"y\<in>s - path_component s x" 
    1.63 +  fix y assume as:"y\<in>s - {y. path_component s x y}"
    1.64    then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
    1.65 -  show "\<exists>e>0. ball y e \<subseteq> s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr)
    1.66 -    fix z assume "z\<in>ball y e" "\<not> z \<notin> path_component s x" 
    1.67 -    hence "y \<in> path_component s x" unfolding not_not mem_path_component_set using `e>0` 
    1.68 +  show "\<exists>e>0. ball y e \<subseteq> s - {y. path_component s x y}" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr)
    1.69 +    fix z assume "z\<in>ball y e" "\<not> z \<notin> {y. path_component s x y}"
    1.70 +    hence "y \<in> {y. path_component s x y}" unfolding not_not mem_Collect_eq using `e>0`
    1.71        apply- apply(rule path_component_trans,assumption) apply(rule path_component_of_subset[OF e(2)])
    1.72        apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto
    1.73      thus False using as by auto qed(insert e(2), auto) qed
    1.74 @@ -462,11 +460,11 @@
    1.75    fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
    1.76    assumes "open s" "connected s" shows "path_connected s"
    1.77    unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule)
    1.78 -  fix x y assume "x \<in> s" "y \<in> s" show "y \<in> path_component s x" proof(rule ccontr)
    1.79 -    assume "y \<notin> path_component s x" moreover
    1.80 -    have "path_component s x \<inter> s \<noteq> {}" using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
    1.81 +  fix x y assume "x \<in> s" "y \<in> s" show "y \<in> {y. path_component s x y}" proof(rule ccontr)
    1.82 +    assume "y \<notin> {y. path_component s x y}" moreover
    1.83 +    have "{y. path_component s x y} \<inter> s \<noteq> {}" using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
    1.84      ultimately show False using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
    1.85 -    using assms(2)[unfolded connected_def not_ex, rule_format, of"path_component s x" "s - path_component s x"] by auto
    1.86 +    using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s - {y. path_component s x y}"] by auto
    1.87  qed qed
    1.88  
    1.89  lemma path_connected_continuous_image: