src/HOL/Multivariate_Analysis/Path_Connected.thy
changeset 50935 cfdf19d3ca32
parent 50884 2b21b4e2d7cb
child 51478 270b21f3ae0a
equal deleted inserted replaced
50934:a076e01b803f 50935:cfdf19d3ca32
    55   unfolding path_def path_image_def
    55   unfolding path_def path_image_def
    56   apply (erule connected_continuous_image)
    56   apply (erule connected_continuous_image)
    57   apply (rule convex_connected, rule convex_real_interval)
    57   apply (rule convex_connected, rule convex_real_interval)
    58   done
    58   done
    59 
    59 
    60 lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g :: 'a::metric_space set)"
    60 lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
    61   unfolding path_def path_image_def
    61   unfolding path_def path_image_def
    62   by (erule compact_continuous_image, rule compact_interval)
    62   by (erule compact_continuous_image, rule compact_interval)
    63 
    63 
    64 lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g"
    64 lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g"
    65   unfolding reversepath_def by auto
    65   unfolding reversepath_def by auto