equal
deleted
inserted
replaced
585 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] |
585 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] |
586 by auto |
586 by auto |
587 qed |
587 qed |
588 |
588 |
589 lemma open_path_component: |
589 lemma open_path_component: |
590 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) |
590 fixes s :: "'a::real_normed_vector set" |
591 assumes "open s" |
591 assumes "open s" |
592 shows "open {y. path_component s x y}" |
592 shows "open {y. path_component s x y}" |
593 unfolding open_contains_ball |
593 unfolding open_contains_ball |
594 proof |
594 proof |
595 fix y |
595 fix y |
618 done |
618 done |
619 qed |
619 qed |
620 qed |
620 qed |
621 |
621 |
622 lemma open_non_path_component: |
622 lemma open_non_path_component: |
623 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) |
623 fixes s :: "'a::real_normed_vector set" |
624 assumes "open s" |
624 assumes "open s" |
625 shows "open(s - {y. path_component s x y})" |
625 shows "open(s - {y. path_component s x y})" |
626 unfolding open_contains_ball |
626 unfolding open_contains_ball |
627 proof |
627 proof |
628 fix y |
628 fix y |
646 then show False using as by auto |
646 then show False using as by auto |
647 qed (insert e(2), auto) |
647 qed (insert e(2), auto) |
648 qed |
648 qed |
649 |
649 |
650 lemma connected_open_path_connected: |
650 lemma connected_open_path_connected: |
651 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) |
651 fixes s :: "'a::real_normed_vector set" |
652 assumes "open s" "connected s" |
652 assumes "open s" "connected s" |
653 shows "path_connected s" |
653 shows "path_connected s" |
654 unfolding path_connected_component_set |
654 unfolding path_connected_component_set |
655 proof (rule, rule, rule path_component_subset, rule) |
655 proof (rule, rule, rule path_component_subset, rule) |
656 fix x y |
656 fix x y |