Theory Missing_Topology

theory Missing_Topology
imports Multivariate_Analysis
(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Some useful lemmas in topology›

theory Missing_Topology imports "HOL-Analysis.Multivariate_Analysis"
begin

subsection ‹Misc›    
 
lemma open_times_image:
  fixes S::"'a::real_normed_field set"
  assumes "open S" "c≠0"
  shows "open (((*) c) ` S)" 
proof -
  let ?f = "λx. x/c" and ?g="((*) c)"
  have "continuous_on UNIV ?f" using ‹c≠0› by (auto intro:continuous_intros)
  then have "open (?f -` S)" using ‹open S› by (auto elim:open_vimage)
  moreover have "?g ` S = ?f -` S" using ‹c≠0›
    apply auto
    using image_iff by fastforce
  ultimately show ?thesis by auto
qed   
 
lemma image_linear_greaterThan:
  fixes x::"'a::linordered_field"
  assumes "c≠0"
  shows "((λx. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})"
using ‹c≠0›
  apply (auto simp add:image_iff field_simps)    
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done

lemma image_linear_lessThan:
  fixes x::"'a::linordered_field"
  assumes "c≠0"
  shows "((λx. c*x+b) ` {..<x}) = (if c>0 then {..<c*x+b} else {c*x+b<..})"
using ‹c≠0›
  apply (auto simp add:image_iff field_simps)    
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done    
 
lemma continuous_on_neq_split:
  fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
  assumes "∀x∈s. f x≠y" "continuous_on s f" "connected s"
  shows "(∀x∈s. f x>y) ∨ (∀x∈s. f x<y)" 
proof -
  { fix aa :: 'a and aaa :: 'a
    have "y ∉ f ` s"
      using assms(1) by blast
    then have "(aa ∉ s ∨ y < f aa) ∨ aaa ∉ s ∨ f aaa < y"
      by (meson Topological_Spaces.connected_continuous_image assms(2) assms(3) 
          connectedD_interval image_eqI linorder_not_le) }
  then show ?thesis
    by blast
qed

lemma
  fixes f::"'a::linorder_topology ⇒ 'b::topological_space"
  assumes "continuous_on {a..b} f" "a<b"
  shows continuous_on_at_left:"continuous (at_left b) f" 
    and continuous_on_at_right:"continuous (at_right a) f"
proof -
  have "at b within {..a} = bot" 
  proof -
    have "closed {..a}" by auto
    then have "closure ({..a} - {b}) = {..a}" by (simp add: assms(2) not_le)
    then have "b∉closure ({..a} - {b})" using ‹a<b› by auto
    then show ?thesis using at_within_eq_bot_iff by auto
  qed
  then have "(f ⤏ f b) (at b within {..a})" by auto
  moreover have "(f ⤏ f b) (at b within {a..b})"
    using assms unfolding continuous_on by auto
  moreover have "{..a} ∪ {a..b} = {..b}"
    using ‹a<b› by auto
  ultimately have "(f ⤏ f b) (at b within {..b})" 
    using Lim_Un[of f "f b" b "{..a}" "{a..b}"] by presburger
  then have "(f ⤏ f b) (at b within {..<b})"
    apply (elim tendsto_within_subset)
    by auto
  then show "continuous (at_left b) f" using continuous_within by auto
next
  have "at a within {b..} = bot" 
  proof -
    have "closed {b..}" by auto
    then have "closure ({b..} - {a}) = {b..}" by (simp add: assms(2) not_le)
    then have "a∉closure ({b..} - {a})" using ‹a<b› by auto
    then show ?thesis using at_within_eq_bot_iff by auto
  qed
  then have "(f ⤏ f a) (at a within {b..})" by auto
  moreover have "(f ⤏ f a) (at a within {a..b})"
    using assms unfolding continuous_on by auto
  moreover have "{b..} ∪ {a..b} = {a..}"
    using ‹a<b› by auto
  ultimately have "(f ⤏ f a) (at a within {a..})" 
    using Lim_Un[of f "f a" a "{b..}" "{a..b}"] by presburger
  then have "(f ⤏ f a) (at a within {a<..})"
    apply (elim tendsto_within_subset)
    by auto
  then show "continuous (at_right a) f" using continuous_within by auto
qed 
  
subsection ‹More about @{term eventually}›    
    
lemma eventually_comp_filtermap:
    "eventually (P o f) F ⟷ eventually P (filtermap f F)"
  unfolding comp_def using eventually_filtermap by auto
 
lemma eventually_uminus_at_top_at_bot:
  fixes P::"'a::{ordered_ab_group_add,linorder} ⇒ bool"
  shows "eventually (P o uminus) at_bot ⟷ eventually P at_top"
    "eventually (P o uminus) at_top ⟷ eventually P at_bot"
  unfolding eventually_comp_filtermap
  by (fold at_top_mirror at_bot_mirror,auto)
    
lemma eventually_at_infinityI:
  fixes P::"'a::real_normed_vector ⇒ bool"
  assumes "⋀x. c ≤ norm x ⟹ P x"
  shows "eventually P at_infinity"  
unfolding eventually_at_infinity using assms by auto
   
lemma eventually_at_bot_linorderI:
  fixes c::"'a::linorder"
  assumes "⋀x. x ≤ c ⟹ P x"
  shows "eventually P at_bot"
  using assms by (auto simp: eventually_at_bot_linorder)     

lemma eventually_times_inverse_1:
  fixes f::"'a ⇒ 'b::{field,t2_space}"
  assumes "(f ⤏ c) F" "c≠0"
  shows "∀F x in F. inverse (f x) * f x = 1"
proof -
  have "∀F x in F. f x≠0" 
    using assms tendsto_imp_eventually_ne by blast
  then show ?thesis
    apply (elim eventually_mono)
    by auto
qed  
  
subsection ‹More about @{term filtermap}› 

lemma filtermap_linear_at_within:
  assumes "bij f" and cont: "isCont f a" and open_map: "⋀S. open S ⟹ open (f`S)"
  shows "filtermap f (at a within S) = at (f a) within f`S"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (at a within S))"
  then obtain T where "open T" "a ∈ T" and impP:"∀x∈T. x≠a ⟶ x∈S⟶ P (f x)"
    by (auto simp: eventually_filtermap eventually_at_topological)
  then show "eventually P (at (f a) within f ` S)"
    unfolding eventually_at_topological
    apply (intro exI[of _ "f`T"])
    using ‹bij f› open_map by (metis bij_pointE imageE imageI)  
next
  fix P
  assume "eventually P (at (f a) within f ` S)"
  then obtain T1 where "open T1" "f a ∈ T1" and impP:"∀x∈T1. x≠f a ⟶ x∈f`S⟶ P (x)"
    unfolding eventually_at_topological by auto
  then obtain T2 where "open T2" "a ∈ T2" "(∀x'∈T2. f x' ∈ T1)" 
    using cont[unfolded continuous_at_open,rule_format,of T1] by blast 
  then have "∀x∈T2. x≠a ⟶ x∈S⟶ P (f x)"
    using impP by (metis assms(1) bij_pointE imageI)
  then show "eventually P (filtermap f (at a within S))" 
    unfolding eventually_filtermap eventually_at_topological 
    apply (intro exI[of _ T2])
    using ‹open T2› ‹a ∈ T2› by auto
qed
  
lemma filtermap_at_bot_linear_eq:
  fixes c::"'a::linordered_field"
  assumes "c≠0"
  shows "filtermap (λx. x * c + b) at_bot = (if c>0 then at_bot else at_top)"
proof (cases "c>0")
  case True
  then have "filtermap (λx. x * c + b) at_bot = at_bot" 
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_bot_linorder filterlim_at_bot
      by (auto simp add: field_simps)
    subgoal unfolding eventually_at_bot_linorder filterlim_at_bot
      by (metis mult.commute real_affinity_le)
    by auto
  then show ?thesis using ‹c>0› by auto
next
  case False
  then have "c<0" using ‹c≠0› by auto
  then have "filtermap (λx. x * c + b) at_bot = at_top"
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_top_linorder filterlim_at_bot
      by (meson le_diff_eq neg_divide_le_eq)
    subgoal unfolding eventually_at_bot_linorder filterlim_at_top
      using ‹c < 0› by (meson False diff_le_eq le_divide_eq)
    by auto
  then show ?thesis using ‹c<0› by auto
qed  
  
lemma filtermap_linear_at_left:
  fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}"
  assumes "c≠0"
  shows "filtermap (λx. c*x+b) (at_left x) = (if c>0 then at_left (c*x+b) else at_right (c*x+b))"
proof -
  let ?f = "λx. c*x+b"
  have "filtermap (λx. c*x+b) (at_left x) = (at (?f x) within ?f ` {..<x})"
  proof (subst filtermap_linear_at_within)
    show "bij ?f" using ‹c≠0› 
      by (auto intro!: o_bij[of "λx. (x-b)/c"])
    show "isCont ?f x" by auto
    show "⋀S. open S ⟹ open (?f ` S)" 
      using open_times_image[OF _ ‹c≠0›,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {..<x} = at (?f x) within ?f ` {..<x}" by simp
  qed
  moreover have "?f ` {..<x} =  {..<?f x}" when "c>0" 
    using image_linear_lessThan[OF ‹c≠0›,of b x] that by auto
  moreover have "?f ` {..<x} =  {?f x<..}" when "¬ c>0" 
    using image_linear_lessThan[OF ‹c≠0›,of b x] that by auto
  ultimately show ?thesis by auto
qed
    
lemma filtermap_linear_at_right:
  fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}"
  assumes "c≠0"
  shows "filtermap (λx. c*x+b) (at_right x) = (if c>0 then at_right (c*x+b) else at_left (c*x+b))" 
proof -
  let ?f = "λx. c*x+b"
  have "filtermap ?f (at_right x) = (at (?f x) within ?f ` {x<..})"
  proof (subst filtermap_linear_at_within)
    show "bij ?f" using ‹c≠0› 
      by (auto intro!: o_bij[of "λx. (x-b)/c"])
    show "isCont ?f x" by auto
    show "⋀S. open S ⟹ open (?f ` S)" 
      using open_times_image[OF _ ‹c≠0›,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {x<..} = at (?f x) within ?f ` {x<..}" by simp
  qed
  moreover have "?f ` {x<..} =  {?f x<..}" when "c>0" 
    using image_linear_greaterThan[OF ‹c≠0›,of b x] that by auto
  moreover have "?f ` {x<..} =  {..<?f x}" when "¬ c>0" 
    using image_linear_greaterThan[OF ‹c≠0›,of b x] that by auto
  ultimately show ?thesis by auto
qed
 
lemma filtermap_at_top_linear_eq:
  fixes c::"'a::linordered_field"
  assumes "c≠0"
  shows "filtermap (λx. x * c + b) at_top = (if c>0 then at_top else at_bot)"
proof (cases "c>0")
  case True
  then have "filtermap (λx. x * c + b) at_top = at_top" 
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_top_linorder filterlim_at_top 
      by (meson le_diff_eq pos_le_divide_eq)
    subgoal unfolding eventually_at_top_linorder filterlim_at_top
      apply auto
      by (metis mult.commute real_le_affinity) 
    by auto
  then show ?thesis using ‹c>0› by auto
next
  case False
  then have "c<0" using ‹c≠0› by auto
  then have "filtermap (λx. x * c + b) at_top = at_bot"
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_bot_linorder filterlim_at_top
      by (auto simp add: field_simps)
    subgoal unfolding eventually_at_top_linorder filterlim_at_bot
      by (meson le_diff_eq neg_divide_le_eq)
    by auto
  then show ?thesis using ‹c<0› by auto
qed

  
lemma filtermap_nhds_open_map:
  assumes cont: "isCont f a"
    and open_map: "⋀S. open S ⟹ open (f`S)"
  shows "filtermap f (nhds a) = nhds (f a)"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (nhds a))"
  then obtain S where "open S" "a ∈ S" "∀x∈S. P (f x)"
    by (auto simp: eventually_filtermap eventually_nhds)
  then show "eventually P (nhds (f a))"
    unfolding eventually_nhds 
    apply (intro exI[of _ "f`S"]) 
    by (auto intro!: open_map)
qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
  
subsection ‹More about @{term filterlim}›
  
lemma filterlim_at_infinity_times:
  fixes f :: "'a ⇒ 'b::real_normed_field"
  assumes "filterlim f at_infinity F" "filterlim g at_infinity F"
  shows "filterlim (λx. f x * g x) at_infinity F"  
proof -
  have "((λx. inverse (f x) * inverse (g x)) ⤏ 0 * 0) F"
    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
  then have "filterlim (λx. inverse (f x) * inverse (g x)) (at 0) F"
    unfolding filterlim_at using assms
    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
  then show ?thesis
    by (subst filterlim_inverse_at_iff[symmetric]) simp_all
qed   
  
lemma filterlim_at_top_at_bot[elim]:
  fixes f::"'a ⇒ 'b::unbounded_dense_linorder" and F::"'a filter"
  assumes top:"filterlim f at_top F" and bot: "filterlim f at_bot F" and "F≠bot"
  shows False
proof -
  obtain c::'b where True by auto
  have "∀F x in F. c < f x" 
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀F x in F. f x < c" 
    using bot unfolding filterlim_at_bot_dense by auto
  ultimately have "∀F x in F. c < f x ∧ f x < c" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed  

lemma filterlim_at_top_nhds[elim]:      
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" and "F≠bot"
  shows False
proof -
  obtain c'::'b where "c'>c" using gt_ex by blast
  have "∀F x in F. c' < f x" 
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀F x in F. f x < c'" 
    using order_tendstoD[OF tendsto,of c'] ‹c'>c› by auto
  ultimately have "∀F x in F. c' < f x ∧ f x < c'" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma filterlim_at_bot_nhds[elim]:      
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" and "F≠bot"
  shows False
proof -
  obtain c'::'b where "c'<c" using lt_ex by blast
  have "∀F x in F. c' > f x" 
    using top unfolding filterlim_at_bot_dense by auto
  moreover have "∀F x in F. f x > c'" 
    using order_tendstoD[OF tendsto,of c'] ‹c'<c› by auto
  ultimately have "∀F x in F. c' < f x ∧ f x < c'" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed  
  
lemma filterlim_at_top_linear_iff:
  fixes f::"'a::linordered_field ⇒ 'b"
  assumes "c≠0"
  shows "(LIM x at_top. f (x * c + b) :> F2) ⟷ (if c>0 then (LIM x at_top. f x :> F2) 
            else (LIM x at_bot. f x :> F2))"
  unfolding filterlim_def
  apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric])
  using assms by (auto simp add:filtermap_at_top_linear_eq)
    
lemma filterlim_at_bot_linear_iff:
  fixes f::"'a::linordered_field ⇒ 'b"
  assumes "c≠0"
  shows "(LIM x at_bot. f (x * c + b) :> F2) ⟷ (if c>0 then (LIM x at_bot. f x :> F2) 
            else (LIM x at_top. f x :> F2)) "
  unfolding filterlim_def 
  apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric])
  using assms by (auto simp add:filtermap_at_bot_linear_eq)      
  
  
lemma filterlim_tendsto_add_at_top_iff:
  assumes f: "(f ⤏ c) F"
  shows "(LIM x F. (f x + g x :: real) :> at_top) ⟷ (LIM x F. g x :> at_top)"
proof     
  assume "LIM x F. f x + g x :> at_top" 
  moreover have "((λx. - f x) ⤏ - c) F"
    using f by (intro tendsto_intros,simp)
  ultimately show "filterlim g at_top F" using filterlim_tendsto_add_at_top 
    by fastforce
qed (auto simp add:filterlim_tendsto_add_at_top[OF f])    
    
  
lemma filterlim_tendsto_add_at_bot_iff:
  fixes c::real
  assumes f: "(f ⤏ c) F"
  shows "(LIM x F. f x + g x :> at_bot) ⟷ (LIM x F. g x :> at_bot)" 
proof -
  have "(LIM x F. f x + g x :> at_bot) 
        ⟷  (LIM x F. - f x + (- g x)  :> at_top)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  also have "... = (LIM x F. - g x  :> at_top)"
    apply (subst filterlim_tendsto_add_at_top_iff[of _ "-c"])
    by (auto intro:tendsto_intros simp add:f)
  also have "... = (LIM x F. g x  :> at_bot)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  finally show ?thesis .
qed
  
lemma tendsto_inverse_0_at_infinity: 
    "LIM x F. f x :> at_infinity ⟹ ((λx. inverse (f x) :: real) ⤏ 0) F"
  by (metis filterlim_at filterlim_inverse_at_iff)

lemma filterlim_at_infinity_divide_iff:
  fixes f::"'a ⇒ 'b::real_normed_field"
  assumes "(f ⤏ c) F" "c≠0"
  shows "(LIM x F. f x / g x :> at_infinity) ⟷ (LIM x F. g x :> at 0)"
proof 
  assume asm:"LIM x F. f x / g x :> at_infinity"
  have "LIM x F. inverse (f x) * (f x / g x) :> at_infinity"
    apply (rule tendsto_mult_filterlim_at_infinity[of _ "inverse c", OF _ _ asm])
    by (auto simp add: assms(1) assms(2) tendsto_inverse)
  then have "LIM x F. inverse (g x) :> at_infinity"
    apply (elim filterlim_mono_eventually)
    using eventually_times_inverse_1[OF assms] 
    by (auto elim:eventually_mono simp add:field_simps)
  then show "filterlim g (at 0) F" using filterlim_inverse_at_iff[symmetric] by force 
next
  assume "filterlim g (at 0) F" 
  then have "filterlim (λx. inverse (g x)) at_infinity F"
    using filterlim_compose filterlim_inverse_at_infinity by blast
  then have "LIM x F. f x * inverse (g x) :> at_infinity"
    using tendsto_mult_filterlim_at_infinity[OF assms, of "λx. inverse(g x)"] 
    by simp
  then show "LIM x F. f x / g x :> at_infinity" by (simp add: divide_inverse)
qed  
  
lemma filterlim_tendsto_pos_mult_at_top_iff:
  fixes f::"'a ⇒ real"
  assumes "(f ⤏ c) F" and "0 < c"
  shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_top)"
proof 
  assume "filterlim g at_top F"
  then show "LIM x F. f x * g x :> at_top" 
    using filterlim_tendsto_pos_mult_at_top[OF assms] by auto
next
  assume asm:"LIM x F. f x * g x :> at_top"
  have "((λx. inverse (f x)) ⤏ inverse c) F" 
    using tendsto_inverse[OF assms(1)] ‹0<c› by auto
  moreover have "inverse c >0" using assms(2) by auto
  ultimately have "LIM x F. inverse (f x) * (f x * g x) :> at_top"
    using filterlim_tendsto_pos_mult_at_top[OF _ _ asm,of "λx. inverse (f x)" "inverse c"] by auto
  then show "LIM x F. g x :> at_top"
    apply (elim filterlim_mono_eventually)
      apply simp_all[2]
    using eventually_times_inverse_1[OF assms(1)] ‹c>0› eventually_mono by fastforce
qed  

lemma filterlim_tendsto_pos_mult_at_bot_iff:
  fixes c :: real
  assumes "(f ⤏ c) F" "0 < c" 
  shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_bot F"
  using filterlim_tendsto_pos_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] 
  unfolding filterlim_uminus_at_bot by simp    

lemma filterlim_tendsto_neg_mult_at_top_iff:
  fixes f::"'a ⇒ real"
  assumes "(f ⤏ c) F" and "c < 0"
  shows "(LIM x F. (f x * g x) :> at_top) ⟷ (LIM x F. g x :> at_bot)"  
proof -
  have "(LIM x F. f x * g x :> at_top) = (LIM x F. - g x :> at_top)"
    apply (rule filterlim_tendsto_pos_mult_at_top_iff[of "λx. - f x" "-c" F "λx. - g x", simplified])
    using assms by (auto intro: tendsto_intros )
  also have "... = (LIM x F. g x :> at_bot)" 
    using filterlim_uminus_at_bot[symmetric] by auto
  finally show ?thesis .
qed

lemma filterlim_tendsto_neg_mult_at_bot_iff:
  fixes c :: real
  assumes "(f ⤏ c) F" "0 > c" 
  shows "(LIM x F. f x * g x :> at_bot) ⟷ filterlim g at_top F"
  using filterlim_tendsto_neg_mult_at_top_iff[OF assms(1,2), of "λx. - g x"] 
  unfolding filterlim_uminus_at_top by simp    

lemma Lim_add:
  fixes f g::"_ ⇒ 'a::{t2_space,topological_monoid_add}"
  assumes "∃y. (f ⤏ y) F" and "∃y. (g ⤏ y) F" and "F≠bot"
  shows "Lim F f + Lim F g = Lim F (λx. f x+g x)"
  apply (rule tendsto_Lim[OF ‹F≠bot›, symmetric])
  apply (auto intro!:tendsto_eq_intros)
  using assms tendsto_Lim by blast+

(*
lemma filterlim_at_top_tendsto[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" 
          and "F≠bot"
  shows False
proof -
  obtain cc where "cc>c" using gt_ex by blast
  have "∀F x in F. cc < f x" 
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀F x in F. f x < cc" 
    using tendsto order_tendstoD(2)[OF _ ‹cc>c›] by auto
  ultimately have "∀F x in F. cc < f x ∧ f x < cc" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma filterlim_at_bot_tendsto[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" 
          and "F≠bot"
  shows False
proof -
  obtain cc where "cc<c" using lt_ex by blast
  have "∀F x in F. cc > f x" 
    using top unfolding filterlim_at_bot_dense by auto
  moreover have "∀F x in F. f x > cc" 
    using tendsto order_tendstoD(1)[OF _ ‹cc<c›] by auto
  ultimately have "∀F x in F. cc < f x ∧ f x < cc" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed
*)
  
subsection ‹Isolate and discrete›  
  
definition (in topological_space) isolate:: "'a ⇒ 'a set ⇒ bool"  (infixr "isolate" 60)
  where "x isolate S ⟷ (x∈S ∧ (∃T. open T ∧ T ∩ S = {x}))"  
    
definition (in topological_space) discrete:: "'a set ⇒ bool" 
  where "discrete S ⟷ (∀x∈S. x isolate 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 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 isolate_islimpt_iff:"(x isolate S) ⟷ (¬ (x islimpt S) ∧ x∈S)"
  unfolding isolate_def islimpt_def by auto
  
lemma isolate_dist_Ex_iff:
  fixes x::"'a::metric_space"
  shows "x isolate S ⟷ (x∈S ∧ (∃e>0. ∀y∈S. dist x y < e ⟶ y=x))"
unfolding isolate_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 isolate_insert: 
  fixes x :: "'a::t1_space"
  shows "x isolate (insert a S) ⟷ x isolate S ∨ (x=a ∧ ¬ (x islimpt S))"
by (meson insert_iff islimpt_insert isolate_islimpt_iff)
    
(*
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 isolate_dist_Ex_iff uniform_discrete_def)
  
lemma isolate_subset:"x isolate S ⟹ T ⊆ S ⟹ x∈T ⟹ x isolate T"
  unfolding isolate_def by fastforce

lemma discrete_subset[elim]: "discrete S ⟹ T ⊆ S ⟹ discrete T"
  unfolding discrete_def using islimpt_subset isolate_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 isolate_islimpt_iff)
   
(* Is euclidean_space really necessary?*)    
lemma uniform_discrete_insert:
  fixes S :: "'a::euclidean_space set"
  shows "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 (simp add: ‹0 < e1› e2_def setdist_gt_0_compact_closed that(1) that(2))
    moreover have "x = y" when "x∈insert a S" "y∈insert a S" "dist x y < e2 " for x y
    proof -
      have ?thesis when "x=a" "y=a" using that by auto
      moreover have ?thesis when "x=a" "y∈S"
        using that setdist_le_dist[of x "{a}" y S] ‹dist x y < e2› unfolding e2_def
        by fastforce
      moreover have ?thesis when "y=a" "x∈S"
        using that setdist_le_dist[of y "{a}" x S] ‹dist x y < e2› unfolding e2_def
        by (simp add: dist_commute)
      moreover have ?thesis when "x∈S" "y∈S"
        using e1_dist[rule_format, OF that] ‹dist x y < e2› unfolding e2_def
        by (simp add: dist_commute)
      ultimately show ?thesis using that by auto
    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 isolate_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 isolate_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_gr_iff all_not_in_conv asm dual_order.irrefl eq_iff finite_imageI imageI 
          less_eq_real_def)
    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:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  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} = {}"
    proof -
      have "S={x1}" using that ‹S≠{}› by auto
      then show ?thesis using uniform_discrete_insert[of "f x1"] by auto
    qed
    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)"
        using dist[rule_format, OF ‹x1∈S› ‹x2∈S›] .
      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" "dist x1 x2 < e " for x1 x2 
    proof -
      obtain y1 where y1:"y1∈S" "x1=f y1" using ‹x1∈ f ` S› by auto
      obtain y2 where y2:"y2∈S" "x2=f y2" using ‹x2∈ f ` S› by auto    
      have "dist y1 y2 < e1"
        using dist[rule_format, OF y1(1) y2(1)] ‹c>0› ‹dist x1 x2 < e› unfolding e_def
        apply (fold y1(2) y2(2))
        by (auto simp add:divide_simps mult.commute) 
      then have "y1=y2"    
        using e1_dist[rule_format, OF y2(1) y1(1)] by simp
      then show "x1=x2" using y1(2) y2(2) by auto
    qed
    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
 

  
end