section ‹Some Uncountable Sets› theory Uncountable_Sets imports Path_Connected Continuum_Not_Denumerable begin lemma uncountable_closed_segment: fixes a :: "'a::real_normed_vector" assumes "a ≠ b" shows "uncountable (closed_segment a b)" unfolding path_image_linepath [symmetric] path_image_def using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1] countable_image_inj_on by auto lemma uncountable_open_segment: fixes a :: "'a::real_normed_vector" assumes "a ≠ b" shows "uncountable (open_segment a b)" by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable) lemma uncountable_convex: fixes a :: "'a::real_normed_vector" assumes "convex S" "a ∈ S" "b ∈ S" "a ≠ b" shows "uncountable S" proof - have "uncountable (closed_segment a b)" by (simp add: uncountable_closed_segment assms) then show ?thesis by (meson assms convex_contains_segment countable_subset) qed lemma uncountable_ball: fixes a :: "'a::euclidean_space" assumes "r > 0" shows "uncountable (ball a r)" proof - have "uncountable (open_segment a (a + r *⇩_{R}(SOME i. i ∈ Basis)))" by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le scale_eq_0_iff uncountable_open_segment) moreover have "open_segment a (a + r *⇩_{R}(SOME i. i ∈ Basis)) ⊆ ball a r" using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis) ultimately show ?thesis by (metis countable_subset) qed lemma ball_minus_countable_nonempty: assumes "countable (A :: 'a :: euclidean_space set)" "r > 0" shows "ball z r - A ≠ {}" proof assume *: "ball z r - A = {}" have "uncountable (ball z r - A)" by (intro uncountable_minus_countable assms uncountable_ball) thus False by (subst (asm) *) auto qed lemma uncountable_cball: fixes a :: "'a::euclidean_space" assumes "r > 0" shows "uncountable (cball a r)" using assms countable_subset uncountable_ball by auto lemma pairwise_disjnt_countable: fixes 𝒩 :: "nat set set" assumes "pairwise disjnt 𝒩" shows "countable 𝒩" by (simp add: assms countable_disjoint_open_subsets open_discrete) lemma pairwise_disjnt_countable_Union: assumes "countable (⋃𝒩)" and pwd: "pairwise disjnt 𝒩" shows "countable 𝒩" proof - obtain f :: "_ ⇒ nat" where f: "inj_on f (⋃𝒩)" using assms by blast then have "pairwise disjnt (⋃ X ∈ 𝒩. {f ` X})" using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f]) then have "countable (⋃ X ∈ 𝒩. {f ` X})" using pairwise_disjnt_countable by blast then show ?thesis by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable) qed lemma connected_uncountable: fixes S :: "'a::metric_space set" assumes "connected S" "a ∈ S" "b ∈ S" "a ≠ b" shows "uncountable S" proof - have "continuous_on S (dist a)" by (intro continuous_intros) then have "connected (dist a ` S)" by (metis connected_continuous_image ‹connected S›) then have "closed_segment 0 (dist a b) ⊆ (dist a ` S)" by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex) then have "uncountable (dist a ` S)" by (metis ‹a ≠ b› countable_subset dist_eq_0_iff uncountable_closed_segment) then show ?thesis by blast qed lemma path_connected_uncountable: fixes S :: "'a::metric_space set" assumes "path_connected S" "a ∈ S" "b ∈ S" "a ≠ b" shows "uncountable S" using path_connected_imp_connected assms connected_uncountable by metis lemma simple_path_image_uncountable: fixes g :: "real ⇒ 'a::metric_space" assumes "simple_path g" shows "uncountable (path_image g)" proof - have "g 0 ∈ path_image g" "g (1/2) ∈ path_image g" by (simp_all add: path_defs) moreover have "g 0 ≠ g (1/2)" using assms by (fastforce simp add: simple_path_def loop_free_def) ultimately have "∀a. ¬ path_image g ⊆ {a}" by blast then show ?thesis using assms connected_simple_path_image connected_uncountable by blast qed lemma arc_image_uncountable: fixes g :: "real ⇒ 'a::metric_space" assumes "arc g" shows "uncountable (path_image g)" by (simp add: arc_imp_simple_path assms simple_path_image_uncountable) end