theory Isolated imports "HOL-Analysis.Elementary_Metric_Spaces" begin subsection ‹Isolate and discrete› definition (in topological_space) isolated_in:: "'a ⇒ 'a set ⇒ bool" (infixr "isolated'_in" 60) where "x isolated_in S ⟷ (x∈S ∧ (∃T. open T ∧ T ∩ S = {x}))" definition (in topological_space) discrete:: "'a set ⇒ bool" where "discrete S ⟷ (∀x∈S. x isolated_in S)" definition (in metric_space) uniform_discrete :: "'a set ⇒ bool" where "uniform_discrete S ⟷ (∃e>0. ∀x∈S. ∀y∈S. dist x y < e ⟶ x = y)" lemma discreteI: "(⋀x. x ∈ X ⟹ x isolated_in X ) ⟹ discrete X" unfolding discrete_def by auto lemma discreteD: "discrete X ⟹ x ∈ X ⟹ x isolated_in X " unfolding discrete_def by auto lemma uniformI1: assumes "e>0" "⋀x y. ⟦x∈S;y∈S;dist x y<e⟧ ⟹ x =y " shows "uniform_discrete S" unfolding uniform_discrete_def using assms by auto lemma uniformI2: assumes "e>0" "⋀x y. ⟦x∈S;y∈S;x≠y⟧ ⟹ dist x y≥e " shows "uniform_discrete S" unfolding uniform_discrete_def using assms not_less by blast lemma isolated_in_islimpt_iff:"(x isolated_in S) ⟷ (¬ (x islimpt S) ∧ x∈S)" unfolding isolated_in_def islimpt_def by auto lemma isolated_in_dist_Ex_iff: fixes x::"'a::metric_space" shows "x isolated_in S ⟷ (x∈S ∧ (∃e>0. ∀y∈S. dist x y < e ⟶ y=x))" unfolding isolated_in_islimpt_iff islimpt_approachable by (metis dist_commute) lemma discrete_empty[simp]: "discrete {}" unfolding discrete_def by auto lemma uniform_discrete_empty[simp]: "uniform_discrete {}" unfolding uniform_discrete_def by (simp add: gt_ex) lemma isolated_in_insert: fixes x :: "'a::t1_space" shows "x isolated_in (insert a S) ⟷ x isolated_in S ∨ (x=a ∧ ¬ (x islimpt S))" by (meson insert_iff islimpt_insert isolated_in_islimpt_iff) lemma isolated_inI: assumes "x∈S" "open T" "T ∩ S = {x}" shows "x isolated_in S" using assms unfolding isolated_in_def by auto lemma isolated_inE: assumes "x isolated_in S" obtains T where "x ∈ S" "open T" "T ∩ S = {x}" using assms that unfolding isolated_in_def by force lemma isolated_inE_dist: assumes "x isolated_in S" obtains d where "d > 0" "⋀y. y ∈ S ⟹ dist x y < d ⟹ y = x" by (meson assms isolated_in_dist_Ex_iff) lemma isolated_in_altdef: "x isolated_in S ⟷ (x∈S ∧ eventually (λy. y ∉ S) (at x))" proof assume "x isolated_in S" from isolated_inE[OF this] obtain T where "x ∈ S" and T:"open T" "T ∩ S = {x}" by metis have "∀⇩_{F}y in nhds x. y ∈ T" apply (rule eventually_nhds_in_open) using T by auto then have "eventually (λy. y ∈ T - {x}) (at x)" unfolding eventually_at_filter by eventually_elim auto then have "eventually (λy. y ∉ S) (at x)" by eventually_elim (use T in auto) then show " x ∈ S ∧ (∀⇩_{F}y in at x. y ∉ S)" using ‹x ∈ S› by auto next assume "x ∈ S ∧ (∀⇩_{F}y in at x. y ∉ S)" then have "∀⇩_{F}y in at x. y ∉ S" "x∈S" by auto from this(1) have "eventually (λy. y ∉ S ∨ y = x) (nhds x)" unfolding eventually_at_filter by eventually_elim auto then obtain T where T:"open T" "x ∈ T" "(∀y∈T. y ∉ S ∨ y = x)" unfolding eventually_nhds by auto with ‹x ∈ S› have "T ∩ S = {x}" by fastforce with ‹x∈S› ‹open T› show "x isolated_in S" unfolding isolated_in_def by auto qed lemma discrete_altdef: "discrete S ⟷ (∀x∈S. ∀⇩_{F}y in at x. y ∉ S)" unfolding discrete_def isolated_in_altdef by auto (* TODO. Other than uniform_discrete S ⟶ discrete S uniform_discrete S ⟶ closed S , we should be able to prove discrete S ∧ closed S ⟶ uniform_discrete S but the proof (based on Tietze Extension Theorem) seems not very trivial to me. Informal proofs can be found in http://topology.auburn.edu/tp/reprints/v30/tp30120.pdf http://msp.org/pjm/1959/9-2/pjm-v9-n2-p19-s.pdf *) lemma uniform_discrete_imp_closed: "uniform_discrete S ⟹ closed S" by (meson discrete_imp_closed uniform_discrete_def) lemma uniform_discrete_imp_discrete: "uniform_discrete S ⟹ discrete S" by (metis discrete_def isolated_in_dist_Ex_iff uniform_discrete_def) lemma isolated_in_subset:"x isolated_in S ⟹ T ⊆ S ⟹ x∈T ⟹ x isolated_in T" unfolding isolated_in_def by fastforce lemma discrete_subset[elim]: "discrete S ⟹ T ⊆ S ⟹ discrete T" unfolding discrete_def using islimpt_subset isolated_in_islimpt_iff by blast lemma uniform_discrete_subset[elim]: "uniform_discrete S ⟹ T ⊆ S ⟹ uniform_discrete T" by (meson subsetD uniform_discrete_def) lemma continuous_on_discrete: "discrete S ⟹ continuous_on S f" unfolding continuous_on_topological by (metis discrete_def islimptI isolated_in_islimpt_iff) lemma uniform_discrete_insert: "uniform_discrete (insert a S) ⟷ uniform_discrete S" proof assume asm:"uniform_discrete S" let ?thesis = "uniform_discrete (insert a S)" have ?thesis when "a∈S" using that asm by (simp add: insert_absorb) moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def) moreover have ?thesis when "a∉S" "S≠{}" proof - obtain e1 where "e1>0" and e1_dist:"∀x∈S. ∀y∈S. dist y x < e1 ⟶ y = x" using asm unfolding uniform_discrete_def by auto define e2 where "e2 ≡ min (setdist {a} S) e1" have "closed S" using asm uniform_discrete_imp_closed by auto then have "e2>0" by (smt (verit) ‹0 < e1› e2_def infdist_eq_setdist infdist_pos_not_in_closed that) moreover have "x = y" if "x∈insert a S" "y∈insert a S" "dist x y < e2" for x y proof (cases "x=a ∨ y=a") case True then show ?thesis by (smt (verit, best) dist_commute e2_def infdist_eq_setdist infdist_le insertE that) next case False then show ?thesis using e1_dist e2_def that by force qed ultimately show ?thesis unfolding uniform_discrete_def by meson qed ultimately show ?thesis by auto qed (simp add: subset_insertI uniform_discrete_subset) lemma discrete_compact_finite_iff: fixes S :: "'a::t1_space set" shows "discrete S ∧ compact S ⟷ finite S" proof assume "finite S" then have "compact S" using finite_imp_compact by auto moreover have "discrete S" unfolding discrete_def using isolated_in_islimpt_iff islimpt_finite[OF ‹finite S›] by auto ultimately show "discrete S ∧ compact S" by auto next assume "discrete S ∧ compact S" then show "finite S" by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolated_in_islimpt_iff order_refl) qed lemma uniform_discrete_finite_iff: fixes S :: "'a::heine_borel set" shows "uniform_discrete S ∧ bounded S ⟷ finite S" proof assume "uniform_discrete S ∧ bounded S" then have "discrete S" "compact S" using uniform_discrete_imp_discrete uniform_discrete_imp_closed compact_eq_bounded_closed by auto then show "finite S" using discrete_compact_finite_iff by auto next assume asm:"finite S" let ?thesis = "uniform_discrete S ∧ bounded S" have ?thesis when "S={}" using that by auto moreover have ?thesis when "S≠{}" proof - have "∀x. ∃d>0. ∀y∈S. y ≠ x ⟶ d ≤ dist x y" using finite_set_avoid[OF ‹finite S›] by auto then obtain f where f_pos:"f x>0" and f_dist: "∀y∈S. y ≠ x ⟶ f x ≤ dist x y" if "x∈S" for x by metis define f_min where "f_min ≡ Min (f ` S)" have "f_min > 0" unfolding f_min_def by (simp add: asm f_pos that) moreover have "∀x∈S. ∀y∈S. f_min > dist x y ⟶ x=y" using f_dist unfolding f_min_def by (metis Min_le asm finite_imageI imageI le_less_trans linorder_not_less) ultimately have "uniform_discrete S" unfolding uniform_discrete_def by auto moreover have "bounded S" using ‹finite S› by auto ultimately show ?thesis by auto qed ultimately show ?thesis by blast qed lemma uniform_discrete_image_scale: assumes "uniform_discrete S" and dist:"∀x∈S. ∀y∈S. dist x y = c * dist (f x) (f y)" shows "uniform_discrete (f ` S)" proof - have ?thesis when "S={}" using that by auto moreover have ?thesis when "S≠{}" "c≤0" proof - obtain x1 where "x1∈S" using ‹S≠{}› by auto have ?thesis when "S-{x1} = {}" using ‹x1 ∈ S› subset_antisym that uniform_discrete_insert by fastforce moreover have ?thesis when "S-{x1} ≠ {}" proof - obtain x2 where "x2∈S-{x1}" using ‹S-{x1} ≠ {}› by auto then have "x2∈S" "x1≠x2" by auto then have "dist x1 x2 > 0" by auto moreover have "dist x1 x2 = c * dist (f x1) (f x2)" by (simp add: ‹x1 ∈ S› ‹x2 ∈ S› dist) moreover have "dist (f x2) (f x2) ≥ 0" by auto ultimately have False using ‹c≤0› by (simp add: zero_less_mult_iff) then show ?thesis by auto qed ultimately show ?thesis by auto qed moreover have ?thesis when "S≠{}" "c>0" proof - obtain e1 where "e1>0" and e1_dist:"∀x∈S. ∀y∈S. dist y x < e1 ⟶ y = x" using ‹uniform_discrete S› unfolding uniform_discrete_def by auto define e where "e ≡ e1/c" have "x1 = x2" when "x1 ∈ f ` S" "x2 ∈ f ` S" and d: "dist x1 x2 < e" for x1 x2 by (smt (verit) ‹0 < c› d dist divide_right_mono e1_dist e_def imageE nonzero_mult_div_cancel_left that) moreover have "e>0" using ‹e1>0› ‹c>0› unfolding e_def by auto ultimately show ?thesis unfolding uniform_discrete_def by meson qed ultimately show ?thesis by fastforce qed definition sparse :: "real ⇒ 'a :: metric_space set ⇒ bool" where "sparse ε X ⟷ (∀x∈X. ∀y∈X-{x}. dist x y > ε)" lemma sparse_empty [simp, intro]: "sparse ε {}" by (auto simp: sparse_def) lemma sparseI [intro?]: "(⋀x y. x ∈ X ⟹ y ∈ X ⟹ x ≠ y ⟹ dist x y > ε) ⟹ sparse ε X" unfolding sparse_def by auto lemma sparseD: "sparse ε X ⟹ x ∈ X ⟹ y ∈ X ⟹ x ≠ y ⟹ dist x y > ε" unfolding sparse_def by auto lemma sparseD': "sparse ε X ⟹ x ∈ X ⟹ y ∈ X ⟹ dist x y ≤ ε ⟹ x = y" unfolding sparse_def by force lemma sparse_singleton [simp, intro]: "sparse ε {x}" by (auto simp: sparse_def) definition setdist_gt where "setdist_gt ε X Y ⟷ (∀x∈X. ∀y∈Y. dist x y > ε)" lemma setdist_gt_empty [simp]: "setdist_gt ε {} Y" "setdist_gt ε X {}" by (auto simp: setdist_gt_def) lemma setdist_gtI: "(⋀x y. x ∈ X ⟹ y ∈ Y ⟹ dist x y > ε) ⟹ setdist_gt ε X Y" unfolding setdist_gt_def by auto lemma setdist_gtD: "setdist_gt ε X Y ⟹ x ∈ X ⟹ y ∈ Y ⟹ dist x y > ε" unfolding setdist_gt_def by auto lemma setdist_gt_setdist: "ε < setdist A B ⟹ setdist_gt ε A B" unfolding setdist_gt_def using setdist_le_dist by fastforce lemma setdist_gt_mono: "setdist_gt ε' A B ⟹ ε ≤ ε' ⟹ A' ⊆ A ⟹ B' ⊆ B ⟹ setdist_gt ε A' B'" by (force simp: setdist_gt_def) lemma setdist_gt_Un_left: "setdist_gt ε (A ∪ B) C ⟷ setdist_gt ε A C ∧ setdist_gt ε B C" by (auto simp: setdist_gt_def) lemma setdist_gt_Un_right: "setdist_gt ε C (A ∪ B) ⟷ setdist_gt ε C A ∧ setdist_gt ε C B" by (auto simp: setdist_gt_def) lemma compact_closed_imp_eventually_setdist_gt_at_right_0: assumes "compact A" "closed B" "A ∩ B = {}" shows "eventually (λε. setdist_gt ε A B) (at_right 0)" proof (cases "A = {} ∨ B = {}") case False hence "setdist A B > 0" by (metis IntI assms empty_iff in_closed_iff_infdist_zero order_less_le setdist_attains_inf setdist_pos_le setdist_sym) hence "eventually (λε. ε < setdist A B) (at_right 0)" using eventually_at_right_field by blast thus ?thesis by eventually_elim (auto intro: setdist_gt_setdist) qed auto lemma setdist_gt_symI: "setdist_gt ε A B ⟹ setdist_gt ε B A" by (force simp: setdist_gt_def dist_commute) lemma setdist_gt_sym: "setdist_gt ε A B ⟷ setdist_gt ε B A" by (force simp: setdist_gt_def dist_commute) lemma eventually_setdist_gt_at_right_0_mult_iff: assumes "c > 0" shows "eventually (λε. setdist_gt (c * ε) A B) (at_right 0) ⟷ eventually (λε. setdist_gt ε A B) (at_right 0)" proof - have "eventually (λε. setdist_gt (c * ε) A B) (at_right 0) ⟷ eventually (λε. setdist_gt ε A B) (filtermap ((*) c) (at_right 0))" by (simp add: eventually_filtermap) also have "filtermap ((*) c) (at_right 0) = at_right 0" by (subst filtermap_times_pos_at_right) (use assms in auto) finally show ?thesis . qed end