Theory Elementary_Topology

(*  Author:     L C Paulson, University of Cambridge
    Author:     Amine Chaieb, University of Cambridge
    Author:     Robert Himmelmann, TU Muenchen
    Author:     Brian Huffman, Portland State University
*)

chapter Topology

theory Elementary_Topology
imports
  "HOL-Library.Set_Idioms"
  "HOL-Library.Disjoint_Sets"
  Product_Vector
begin


section Elementary Topology


subsubsectiontag unimportant Affine transformations of intervals

lemma real_affinity_le: "0 < m  m * x + c  y  x  inverse m * y + - (c / m)"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)

lemma real_le_affinity: "0 < m  y  m * x + c  inverse m * y + - (c / m)  x"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)

lemma real_affinity_lt: "0 < m  m * x + c < y  x < inverse m * y + - (c / m)"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)

lemma real_lt_affinity: "0 < m  y < m * x + c  inverse m * y + - (c / m) < x"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)

lemma real_affinity_eq: "m  0  m * x + c = y  x = inverse m * y + - (c / m)"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)

lemma real_eq_affinity: "m  0  y = m * x + c   inverse m * y + - (c / m) = x"
  for m :: "'a::linordered_field"
  by (simp add: field_simps)


subsection Topological Basis

context topological_space
begin

definitiontag important "topological_basis B 
  (bB. open b)  (x. open x  (B'. B'  B  B' = x))"

lemma topological_basis:
  "topological_basis B  (x. open x  (B'. B'  B  B' = x))"
  unfolding topological_basis_def
  apply safe
     apply fastforce
    apply fastforce
   apply (erule_tac x=x in allE, simp)
   apply (rule_tac x="{x}" in exI, auto)
  done

lemma topological_basis_iff:
  assumes "B'. B'  B  open B'"
  shows "topological_basis B  (O'. open O'  (xO'. B'B. x  B'  B'  O'))"
    (is "_  ?rhs")
proof safe
  fix O' and x::'a
  assume H: "topological_basis B" "open O'" "x  O'"
  then have "(B'B. B' = O')" by (simp add: topological_basis_def)
  then obtain B' where "B'  B" "O' = B'" by auto
  then show "B'B. x  B'  B'  O'" using H by auto
next
  assume H: ?rhs
  show "topological_basis B"
    using assms unfolding topological_basis_def
  proof safe
    fix O' :: "'a set"
    assume "open O'"
    with H obtain f where "xO'. f x  B  x  f x  f x  O'"
      by (force intro: bchoice simp: Bex_def)
    then show "B'B. B' = O'"
      by (auto intro: exI[where x="{f x |x. x  O'}"])
  qed
qed

lemma topological_basisI:
  assumes "B'. B'  B  open B'"
    and "O' x. open O'  x  O'  B'B. x  B'  B'  O'"
  shows "topological_basis B"
  using assms by (subst topological_basis_iff) auto

lemma topological_basisE:
  fixes O'
  assumes "topological_basis B"
    and "open O'"
    and "x  O'"
  obtains B' where "B'  B" "x  B'" "B'  O'"
proof atomize_elim
  from assms have "B'. B'B  open B'"
    by (simp add: topological_basis_def)
  with topological_basis_iff assms
  show  "B'. B'  B  x  B'  B'  O'"
    using assms by (simp add: Bex_def)
qed

lemma topological_basis_open:
  assumes "topological_basis B"
    and "X  B"
  shows "open X"
  using assms by (simp add: topological_basis_def)

lemma topological_basis_imp_subbasis:
  assumes B: "topological_basis B"
  shows "open = generate_topology B"
proof (intro ext iffI)
  fix S :: "'a set"
  assume "open S"
  with B obtain B' where "B'  B" "S = B'"
    unfolding topological_basis_def by blast
  then show "generate_topology B S"
    by (auto intro: generate_topology.intros dest: topological_basis_open)
next
  fix S :: "'a set"
  assume "generate_topology B S"
  then show "open S"
    by induct (auto dest: topological_basis_open[OF B])
qed

lemma basis_dense:
  fixes B :: "'a set set"
    and f :: "'a set  'a"
  assumes "topological_basis B"
    and choosefrom_basis: "B'. B'  {}  f B'  B'"
  shows "X. open X  X  {}  (B'  B. f B'  X)"
proof (intro allI impI)
  fix X :: "'a set"
  assume "open X" and "X  {}"
  from topological_basisE[OF topological_basis B open X choosefrom_basis[OF X  {}]]
  obtain B' where "B'  B" "f X  B'" "B'  X" .
  then show "B'B. f B'  X"
    by (auto intro!: choosefrom_basis)
qed

end

lemma topological_basis_prod:
  assumes A: "topological_basis A"
    and B: "topological_basis B"
  shows "topological_basis ((λ(a, b). a × b) ` (A × B))"
  unfolding topological_basis_def
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
  fix S :: "('a × 'b) set"
  assume "open S"
  then show "XA × B. ((a,b)X. a × b) = S"
  proof (safe intro!: exI[of _ "{xA × B. fst x × snd x  S}"])
    fix x y
    assume "(x, y)  S"
    from open_prod_elim[OF open S this]
    obtain a b where a: "open a""x  a" and b: "open b" "y  b" and "a × b  S"
      by (metis mem_Sigma_iff)
    moreover
    from A a obtain A0 where "A0  A" "x  A0" "A0  a"
      by (rule topological_basisE)
    moreover
    from B b obtain B0 where "B0  B" "y  B0" "B0  b"
      by (rule topological_basisE)
    ultimately show "(x, y)  ((a, b){X  A × B. fst X × snd X  S}. a × b)"
      by (intro UN_I[of "(A0, B0)"]) auto
  qed auto
qed (metis A B topological_basis_open open_Times)


subsection Countable Basis

localetag important countable_basis = topological_space p for p::"'a set  bool" +
  fixes B :: "'a set set"
  assumes is_basis: "topological_basis B"
    and countable_basis: "countable B"
begin

lemma open_countable_basis_ex:
  assumes "p X"
  shows "B'  B. X = B'"
  using assms countable_basis is_basis
  unfolding topological_basis_def by blast

lemma open_countable_basisE:
  assumes "p X"
  obtains B' where "B'  B" "X = B'"
  using assms open_countable_basis_ex
  by atomize_elim simp

lemma countable_dense_exists:
  "D::'a set. countable D  (X. p X  X  {}  (d  D. d  X))"
proof -
  let ?f = "(λB'. SOME x. x  B')"
  have "countable (?f ` B)" using countable_basis by simp
  with basis_dense[OF is_basis, of ?f] show ?thesis
    by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
qed

lemma countable_dense_setE:
  obtains D :: "'a set"
  where "countable D" "X. p X  X  {}  d  D. d  X"
  using countable_dense_exists by blast

end

lemma countable_basis_openI: "countable_basis open B"
  if "countable B" "topological_basis B"
  using that
  by unfold_locales
    (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms)

lemma (in first_countable_topology) first_countable_basisE:
  fixes x :: 'a
  obtains 𝒜 where "countable 𝒜" "A. A  𝒜  x  A" "A. A  𝒜  open A"
    "S. open S  x  S  (A𝒜. A  S)"
proof -
  obtain 𝒜 where 𝒜: "(i::nat. x  𝒜 i  open (𝒜 i))" "(S. open S  x  S  (i. 𝒜 i  S))"
    using first_countable_basis[of x] by metis
  show thesis
  proof 
    show "countable (range 𝒜)"
      by simp
  qed (use 𝒜 in auto)
qed

lemma (in first_countable_topology) first_countable_basis_Int_stableE:
  obtains 𝒜 where "countable 𝒜" "A. A  𝒜  x  A" "A. A  𝒜  open A"
    "S. open S  x  S  (A𝒜. A  S)"
    "A B. A  𝒜  B  𝒜  A  B  𝒜"
proof atomize_elim
  obtain  where :
    "countable "
    "B. B    x  B"
    "B. B    open B"
    "S. open S  x  S  B. B  S"
    by (rule first_countable_basisE) blast
  define 𝒜 where [abs_def]:
    "𝒜 = (λN. ((λn. from_nat_into  n) ` N)) ` (Collect finite::nat set set)"
  then show "𝒜. countable 𝒜  (A. A  𝒜  x  A)  (A. A  𝒜  open A) 
        (S. open S  x  S  (A𝒜. A  S))  (A B. A  𝒜  B  𝒜  A  B  𝒜)"
  proof (safe intro!: exI[where x=𝒜])
    show "countable 𝒜"
      unfolding 𝒜_def by (intro countable_image countable_Collect_finite)
    fix A
    assume "A  𝒜"
    then show "x  A" "open A"
      using (4)[OF open_UNIV] by (auto simp: 𝒜_def intro:  from_nat_into)
  next
    let ?int = "λN. (from_nat_into  ` N)"
    fix A B
    assume "A  𝒜" "B  𝒜"
    then obtain N M where "A = ?int N" "B = ?int M" "finite (N  M)"
      by (auto simp: 𝒜_def)
    then show "A  B  𝒜"
      by (auto simp: 𝒜_def intro!: image_eqI[where x="N  M"])
  next
    fix S
    assume "open S" "x  S"
    then obtain a where a: "a" "a  S" using  by blast
    then show "a𝒜. a  S" using a 
      by (intro bexI[where x=a]) (auto simp: 𝒜_def intro: image_eqI[where x="{to_nat_on  a}"])
  qed
qed

lemma (in topological_space) first_countableI:
  assumes "countable 𝒜"
    and 1: "A. A  𝒜  x  A" "A. A  𝒜  open A"
    and 2: "S. open S  x  S  A𝒜. A  S"
  shows "𝒜::nat  'a set. (i. x  𝒜 i  open (𝒜 i))  (S. open S  x  S  (i. 𝒜 i  S))"
proof (safe intro!: exI[of _ "from_nat_into 𝒜"])
  fix i
  have "𝒜  {}" using 2[of UNIV] by auto
  show "x  from_nat_into 𝒜 i" "open (from_nat_into 𝒜 i)"
    using range_from_nat_into_subset[OF 𝒜  {}] 1 by auto
next
  fix S
  assume "open S" "xS" from 2[OF this]
  show "i. from_nat_into 𝒜 i  S"
    using subset_range_from_nat_into[OF countable 𝒜] by auto
qed

instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
proof
  fix x :: "'a × 'b"
  obtain 𝒜 where 𝒜:
      "countable 𝒜"
      "a. a  𝒜  fst x  a"
      "a. a  𝒜  open a"
      "S. open S  fst x  S  a𝒜. a  S"
    by (rule first_countable_basisE[of "fst x"]) blast
  obtain B where B:
      "countable B"
      "a. a  B  snd x  a"
      "a. a  B  open a"
      "S. open S  snd x  S  aB. a  S"
    by (rule first_countable_basisE[of "snd x"]) blast
  show "𝒜::nat  ('a × 'b) set.
    (i. x  𝒜 i  open (𝒜 i))  (S. open S  x  S  (i. 𝒜 i  S))"
  proof (rule first_countableI[of "(λ(a, b). a × b) ` (𝒜 × B)"], safe)
    fix a b
    assume x: "a  𝒜" "b  B"
    show "x  a × b" 
      by (simp add: 𝒜(2) B(2) mem_Times_iff x)
    show "open (a × b)"
      by (simp add: 𝒜(3) B(3) open_Times x)
  next
    fix S
    assume "open S" "x  S"
    then obtain a' b' where a'b': "open a'" "open b'" "x  a' × b'" "a' × b'  S"
      by (rule open_prod_elim)
    moreover
    from a'b' 𝒜(4)[of a'] B(4)[of b']
    obtain a b where "a  𝒜" "a  a'" "b  B" "b  b'"
      by auto
    ultimately
    show "a(λ(a, b). a × b) ` (𝒜 × B). a  S"
      by (auto intro!: bexI[of _ "a × b"] bexI[of _ a] bexI[of _ b])
  qed (simp add: 𝒜 B)
qed

class second_countable_topology = topological_space +
  assumes ex_countable_subbasis:
    "B::'a set set. countable B  open = generate_topology B"
begin

lemma ex_countable_basis: "B::'a set set. countable B  topological_basis B"
proof -
  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
    by blast
  let ?B = "Inter ` {b. finite b  b  B }"

  show ?thesis
  proof (intro exI conjI)
    show "countable ?B"
      by (intro countable_image countable_Collect_finite_subset B)
    {
      fix S
      assume "open S"
      then have "B'{b. finite b  b  B}. (bB'. b) = S"
        unfolding B
      proof induct
        case UNIV
        show ?case by (intro exI[of _ "{{}}"]) simp
      next
        case (Int a b)
        then obtain x y where x: "a = (Inter ` x)" "i. i  x  finite i  i  B"
          and y: "b = (Inter ` y)" "i. i  y  finite i  i  B"
          by blast
        show ?case
          unfolding x y Int_UN_distrib2
          by (intro exI[of _ "{i  j| i j.  i  x  j  y}"]) (auto dest: x(2) y(2))
      next
        case (UN K)
        then have "kK. B'{b. finite b  b  B}.  (Inter ` B') = k" by auto
        then obtain k where
            "kaK. k ka  {b. finite b  b  B}  (Inter ` (k ka)) = ka"
          unfolding bchoice_iff ..
        then show "B'{b. finite b  b  B}.  (Inter ` B') = K"
          by (intro exI[of _ "(k ` K)"]) auto
      next
        case (Basis S)
        then show ?case
          by (intro exI[of _ "{{S}}"]) auto
      qed
      then have "(B'Inter ` {b. finite b  b  B}. B' = S)"
        unfolding subset_image_iff by blast }
    then show "topological_basis ?B"
      unfolding topological_basis_def
      by (safe intro!: open_Inter)
         (simp_all add: B generate_topology.Basis subset_eq)
  qed
qed


end

lemma univ_second_countable:
  obtains  :: "'a::second_countable_topology set set"
  where "countable " "C. C    open C"
       "S. open S  U. U    S = U"
by (metis ex_countable_basis topological_basis_def)

proposition Lindelof:
  fixes  :: "'a::second_countable_topology set set"
  assumes : "S. S    open S"
  obtains ℱ' where "ℱ'  " "countable ℱ'" "ℱ' = "
proof -
  obtain  :: "'a set set"
    where "countable " "C. C    open C"
      and : "S. open S  U. U    S = U"
    using univ_second_countable by blast
  define 𝒟 where "𝒟  {S. S    (U. U    S  U)}"
  have "countable 𝒟"
    apply (rule countable_subset [OF _ countable ])
    apply (force simp: 𝒟_def)
    done
  have "S. U. S  𝒟  U    S  U"
    by (simp add: 𝒟_def)
  then obtain G where G: "S. S  𝒟  G S    S  G S"
    by metis
  have "  𝒟"
    unfolding 𝒟_def by (blast dest:  )
  moreover have "𝒟  "
    using 𝒟_def by blast
  ultimately have eq1: " = 𝒟" ..
  have eq2: "𝒟 =  (G ` 𝒟)"
    using G eq1 by auto
  show ?thesis
    apply (rule_tac ℱ' = "G ` 𝒟" in that)
    using G countable 𝒟
    by (auto simp: eq1 eq2)
qed

lemma countable_disjoint_open_subsets:
  fixes  :: "'a::second_countable_topology set set"
  assumes "S. S    open S" and pw: "pairwise disjnt "
    shows "countable "
proof -
  obtain ℱ' where "ℱ'  " "countable ℱ'" "ℱ' = "
    by (meson assms Lindelof)
  with pw have "  insert {} ℱ'"
    by (fastforce simp add: pairwise_def disjnt_iff)
  then show ?thesis
    by (simp add: countable ℱ' countable_subset)
qed

sublocale second_countable_topology <
  countable_basis "open" "SOME B. countable B  topological_basis B"
  using someI_ex[OF ex_countable_basis]
  by unfold_locales safe


instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
proof
  obtain A :: "'a set set" where "countable A" "topological_basis A"
    using ex_countable_basis by auto
  moreover
  obtain B :: "'b set set" where "countable B" "topological_basis B"
    using ex_countable_basis by auto
  ultimately show "B::('a × 'b) set set. countable B  open = generate_topology B"
    by (auto intro!: exI[of _ "(λ(a, b). a × b) ` (A × B)"] topological_basis_prod
      topological_basis_imp_subbasis)
qed

instance second_countable_topology  first_countable_topology
proof
  fix x :: 'a
  define B :: "'a set set" where "B = (SOME B. countable B  topological_basis B)"
  then have B: "countable B" "topological_basis B"
    using countable_basis is_basis
    by (auto simp: countable_basis is_basis)
  then show "A::nat  'a set.
    (i. x  A i  open (A i))  (S. open S  x  S  (i. A i  S))"
    by (intro first_countableI[of "{bB. x  b}"])
       (fastforce simp: topological_space_class.topological_basis_def)+
qed

instance nat :: second_countable_topology
proof
  show "B::nat set set. countable B  open = generate_topology B"
    by (intro exI[of _ "range lessThan  range greaterThan"]) (auto simp: open_nat_def)
qed

lemma countable_separating_set_linorder1:
  shows "B::('a::{linorder_topology, second_countable_topology} set). countable B  (x y. x < y  (b  B. x < b  b  y))"
proof -
  obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
  define B1 where "B1 = {(LEAST x. x  U)| U. U  A}"
  then have "countable B1" using countable A by (simp add: Setcompr_eq_image)
  define B2 where "B2 = {(SOME x. x  U)| U. U  A}"
  then have "countable B2" using countable A by (simp add: Setcompr_eq_image)
  have "b  B1  B2. x < b  b  y" if "x < y" for x y
  proof (cases)
    assume "z. x < z  z < y"
    then obtain z where z: "x < z  z < y" by auto
    define U where "U = {x<..<y}"
    then have "open U" by simp
    moreover have "z  U" using z U_def by simp
    ultimately obtain V where "V  A" "z  V" "V  U" 
      using topological_basisE[OF topological_basis A] by auto
    define w where "w = (SOME x. x  V)"
    then have "w  V" using z  V by (metis someI2)
    then have "x < w  w  y" using w  V V  U U_def by fastforce
    moreover have "w  B1  B2" using w_def B2_def V  A by auto
    ultimately show ?thesis by auto
  next
    assume "¬(z. x < z  z < y)"
    then have *: "z. z > x  z  y" by auto
    define U where "U = {x<..}"
    then have "open U" by simp
    moreover have "y  U" using x < y U_def by simp
    ultimately obtain "V" where "V  A" "y  V" "V  U" 
      using topological_basisE[OF topological_basis A] by auto
    have "U = {y..}" unfolding U_def using * x < y by auto
    then have "V  {y..}" using V  U by simp
    then have "(LEAST w. w  V) = y" using y  V by (meson Least_equality atLeast_iff subsetCE)
    then have "y  B1  B2" using V  A B1_def by auto
    moreover have "x < y  y  y" using x < y by simp
    ultimately show ?thesis by auto
  qed
  moreover have "countable (B1  B2)" using countable B1 countable B2 by simp
  ultimately show ?thesis by auto
qed

lemma countable_separating_set_linorder2:
  shows "B::('a::{linorder_topology, second_countable_topology} set). countable B  (x y. x < y  (b  B. x  b  b < y))"
proof -
  obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
  define B1 where "B1 = {(GREATEST x. x  U) | U. U  A}"
  then have "countable B1" using countable A by (simp add: Setcompr_eq_image)
  define B2 where "B2 = {(SOME x. x  U)| U. U  A}"
  then have "countable B2" using countable A by (simp add: Setcompr_eq_image)
  have "b  B1  B2. x  b  b < y" if "x < y" for x y
  proof (cases)
    assume "z. x < z  z < y"
    then obtain z where z: "x < z  z < y" by auto
    define U where "U = {x<..<y}"
    then have "open U" by simp
    moreover have "z  U" using z U_def by simp
    ultimately obtain "V" where "V  A" "z  V" "V  U" 
      using topological_basisE[OF topological_basis A] by auto
    define w where "w = (SOME x. x  V)"
    then have "w  V" using z  V by (metis someI2)
    then have "x  w  w < y" using w  V V  U U_def by fastforce
    moreover have "w  B1  B2" using w_def B2_def V  A by auto
    ultimately show ?thesis by auto
  next
    assume "¬(z. x < z  z < y)"
    then have *: "z. z < y  z  x" using leI by blast
    define U where "U = {..<y}"
    then have "open U" by simp
    moreover have "x  U" using x < y U_def by simp
    ultimately obtain "V" where "V  A" "x  V" "V  U" 
      using topological_basisE[OF topological_basis A] by auto
    have "U = {..x}" unfolding U_def using * x < y by auto
    then have "V  {..x}" using V  U by simp
    then have "(GREATEST x. x  V) = x" using x  V by (meson Greatest_equality atMost_iff subsetCE)
    then have "x  B1  B2" using V  A B1_def by auto
    moreover have "x  x  x < y" using x < y by simp
    ultimately show ?thesis by auto
  qed
  moreover have "countable (B1  B2)" using countable B1 countable B2 by simp
  ultimately show ?thesis by auto
qed

lemma countable_separating_set_dense_linorder:
  shows "B::('a::{linorder_topology, dense_linorder, second_countable_topology} set). countable B  (x y. x < y  (b  B. x < b  b < y))"
proof -
  obtain B::"'a set" where B: "countable B" "x y. x < y  (b  B. x < b  b  y)"
    using countable_separating_set_linorder1 by auto
  have "b  B. x < b  b < y" if "x < y" for x y
  proof -
    obtain z where "x < z" "z < y" using x < y dense by blast
    then obtain b where "b  B" "x < b  b  z" using B(2) by auto
    then have "x < b  b < y" using z < y by auto
    then show ?thesis using b  B by auto
  qed
  then show ?thesis using B(1) by auto
qed


subsection Polish spaces

text Textbooks define Polish spaces as completely metrizable.
  We assume the topology to be complete for a given metric.

class polish_space = complete_space + second_countable_topology


subsection Limit Points

definitiontag important (in topological_space) islimpt:: "'a  'a set  bool"  (infixr "islimpt" 60)
  where "x islimpt S  (T. xT  open T  (yS. yT  yx))"

lemma islimptI:
  assumes "T. x  T  open T  yS. y  T  y  x"
  shows "x islimpt S"
  using assms unfolding islimpt_def by auto

lemma islimptE:
  assumes "x islimpt S" and "x  T" and "open T"
  obtains y where "y  S" and "y  T" and "y  x"
  using assms unfolding islimpt_def by auto

lemma islimpt_iff_eventually: "x islimpt S  ¬ eventually (λy. y  S) (at x)"
  unfolding islimpt_def eventually_at_topological by auto

lemma islimpt_subset: "x islimpt S  S  T  x islimpt T"
  unfolding islimpt_def by fast

lemma islimpt_UNIV_iff: "x islimpt UNIV  ¬ open {x}"
  unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)

lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
  unfolding islimpt_def by blast

text A perfect space has no isolated points.

lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV"
  for x :: "'a::perfect_space"
  unfolding islimpt_UNIV_iff by (rule not_open_singleton)

lemma closed_limpt: "closed S  (x. x islimpt S  x  S)"
  unfolding closed_def
  apply (subst open_subopen)
  apply (simp add: islimpt_def subset_eq)
  apply (metis ComplE ComplI)
  done

lemma islimpt_EMPTY[simp]: "¬ x islimpt {}"
  by (auto simp: islimpt_def)

lemma islimpt_Un: "x islimpt (S  T)  x islimpt S  x islimpt T"
  by (simp add: islimpt_iff_eventually eventually_conj_iff)


lemma islimpt_insert:
  fixes x :: "'a::t1_space"
  shows "x islimpt (insert a s)  x islimpt s"
proof
  assume *: "x islimpt (insert a s)"
  show "x islimpt s"
  proof (rule islimptI)
    fix t
    assume t: "x  t" "open t"
    show "ys. y  t  y  x"
    proof (cases "x = a")
      case True
      obtain y where "y  insert a s" "y  t" "y  x"
        using * t by (rule islimptE)
      with x = a show ?thesis by auto
    next
      case False
      with t have t': "x  t - {a}" "open (t - {a})"
        by (simp_all add: open_Diff)
      obtain y where "y  insert a s" "y  t - {a}" "y  x"
        using * t' by (rule islimptE)
      then show ?thesis by auto
    qed
  qed
next
  assume "x islimpt s"
  then show "x islimpt (insert a s)"
    by (rule islimpt_subset) auto
qed

lemma islimpt_finite:
  fixes x :: "'a::t1_space"
  shows "finite s  ¬ x islimpt s"
  by (induct set: finite) (simp_all add: islimpt_insert)

lemma islimpt_Un_finite:
  fixes x :: "'a::t1_space"
  shows "finite s  x islimpt (s  t)  x islimpt t"
  by (simp add: islimpt_Un islimpt_finite)

lemma islimpt_eq_acc_point:
  fixes l :: "'a :: t1_space"
  shows "l islimpt S  (U. lU  open U  infinite (U  S))"
proof (safe intro!: islimptI)
  fix U
  assume "l islimpt S" "l  U" "open U" "finite (U  S)"
  then have "l islimpt S" "l  (U - (U  S - {l}))" "open (U - (U  S - {l}))"
    by (auto intro: finite_imp_closed)
  then show False
    by (rule islimptE) auto
next
  fix T
  assume *: "U. lU  open U  infinite (U  S)" "l  T" "open T"
  then have "infinite (T  S - {l})"
    by auto
  then have "x. x  (T  S - {l})"
    unfolding ex_in_conv by (intro notI) simp
  then show "yS. y  T  y  l"
    by auto
qed

lemma acc_point_range_imp_convergent_subsequence:
  fixes l :: "'a :: first_countable_topology"
  assumes l: "U. lU  open U  infinite (U  range f)"
  shows "r::natnat. strict_mono r  (f  r)  l"
proof -
  from countable_basis_at_decseq[of l]
  obtain A where A:
      "i. open (A i)"
      "i. l  A i"
      "S. open S  l  S  eventually (λi. A i  S) sequentially"
    by blast
  define s where "s n i = (SOME j. i < j  f j  A (Suc n))" for n i
  {
    fix n i
    have "infinite (A (Suc n)  range f - f`{.. i})"
      using l A by auto
    then have "x. x  A (Suc n)  range f - f`{.. i}"
      unfolding ex_in_conv by (intro notI) simp
    then have "j. f j  A (Suc n)  j  {.. i}"
      by auto
    then have "a. i < a  f a  A (Suc n)"
      by (auto simp: not_le)
    then have "i < s n i" "f (s n i)  A (Suc n)"
      unfolding s_def by (auto intro: someI2_ex)
  }
  note s = this
  define r where "r = rec_nat (s 0 0) s"
  have "strict_mono r"
    by (auto simp: r_def s strict_mono_Suc_iff)
  moreover
  have "(λn. f (r n))  l"
  proof (rule topological_tendstoI)
    fix S
    assume "open S" "l  S"
    with A(3) have "eventually (λi. A i  S) sequentially"
      by auto
    moreover
    {
      fix i
      assume "Suc 0  i"
      then have "f (r i)  A i"
        by (cases i) (simp_all add: r_def s)
    }
    then have "eventually (λi. f (r i)  A i) sequentially"
      by (auto simp: eventually_sequentially)
    ultimately show "eventually (λi. f (r i)  S) sequentially"
      by eventually_elim auto
  qed
  ultimately show "r::natnat. strict_mono r  (f  r)  l"
    by (auto simp: convergent_def comp_def)
qed

lemma islimpt_range_imp_convergent_subsequence:
  fixes l :: "'a :: {t1_space, first_countable_topology}"
  assumes l: "l islimpt (range f)"
  shows "r::natnat. strict_mono r  (f  r)  l"
  using l unfolding islimpt_eq_acc_point
  by (rule acc_point_range_imp_convergent_subsequence)

lemma sequence_unique_limpt:
  fixes f :: "nat  'a::t2_space"
  assumes "(f  l) sequentially"
    and "l' islimpt (range f)"
  shows "l' = l"
proof (rule ccontr)
  assume "l'  l"
  obtain s t where "open s" "open t" "l'  s" "l  t" "s  t = {}"
    using hausdorff [OF l'  l] by auto
  have "eventually (λn. f n  t) sequentially"
    using assms(1) open t l  t by (rule topological_tendstoD)
  then obtain N where "nN. f n  t"
    unfolding eventually_sequentially by auto

  have "UNIV = {..<N}  {N..}"
    by auto
  then have "l' islimpt (f ` ({..<N}  {N..}))"
    using assms(2) by simp
  then have "l' islimpt (f ` {..<N}  f ` {N..})"
    by (simp add: image_Un)
  then have "l' islimpt (f ` {N..})"
    by (simp add: islimpt_Un_finite)
  then obtain y where "y  f ` {N..}" "y  s" "y  l'"
    using l'  s open s by (rule islimptE)
  then obtain n where "N  n" "f n  s" "f n  l'"
    by auto
  with nN. f n  t have "f n  s  t"
    by simp
  with s  t = {} show False
    by simp
qed


subsection Interior of a Set

definitiontag important interior :: "('a::topological_space) set  'a set" where
"interior S = {T. open T  T  S}"

lemma interiorI [intro?]:
  assumes "open T" and "x  T" and "T  S"
  shows "x  interior S"
  using assms unfolding interior_def by fast

lemma interiorE [elim?]:
  assumes "x  interior S"
  obtains T where "open T" and "x  T" and "T  S"
  using assms unfolding interior_def by fast

lemma open_interior [simp, intro]: "open (interior S)"
  by (simp add: interior_def open_Union)

lemma interior_subset: "interior S  S"
  by (auto simp: interior_def)

lemma interior_maximal: "T  S  open T  T  interior S"
  by (auto simp: interior_def)

lemma interior_open: "open S  interior S = S"
  by (intro equalityI interior_subset interior_maximal subset_refl)

lemma interior_eq: "interior S = S  open S"
  by (metis open_interior interior_open)

lemma open_subset_interior: "open S  S  interior T  S  T"
  by (metis interior_maximal interior_subset subset_trans)

lemma interior_empty [simp]: "interior {} = {}"
  using open_empty by (rule interior_open)

lemma interior_UNIV [simp]: "interior UNIV = UNIV"
  using open_UNIV by (rule interior_open)

lemma interior_interior [simp]: "interior (interior S) = interior S"
  using open_interior by (rule interior_open)

lemma interior_mono: "S  T  interior S  interior T"
  by (auto simp: interior_def)

lemma interior_unique:
  assumes "T  S" and "open T"
  assumes "T'. T'  S  open T'  T'  T"
  shows "interior S = T"
  by (intro equalityI assms interior_subset open_interior interior_maximal)

lemma interior_singleton [simp]: "interior {a} = {}"
  for a :: "'a::perfect_space"
  by (meson interior_eq interior_subset not_open_singleton subset_singletonD)

lemma interior_Int [simp]: "interior (S  T) = interior S  interior T"
  by (meson Int_mono Int_subset_iff antisym_conv interior_maximal interior_subset open_Int open_interior)

lemma eventually_nhds_in_nhd: "x  interior s  eventually (λy. y  s) (nhds x)"
  using interior_subset[of s] by (subst eventually_nhds) blast

lemma interior_limit_point [intro]:
  fixes x :: "'a::perfect_space"
  assumes x: "x  interior S"
  shows "x islimpt S"
  using x islimpt_UNIV [of x]
  unfolding interior_def islimpt_def
  apply (clarsimp, rename_tac T T')
  apply (drule_tac x="T  T'" in spec)
  apply (auto simp: open_Int)
  done

lemma interior_closed_Un_empty_interior:
  assumes cS: "closed S"
    and iT: "interior T = {}"
  shows "interior (S  T) = interior S"
proof
  show "interior S  interior (S  T)"
    by (rule interior_mono) (rule Un_upper1)
  show "interior (S  T)  interior S"
  proof
    fix x
    assume "x  interior (S  T)"
    then obtain R where "open R" "x  R" "R  S  T" ..
    show "x  interior S"
    proof (rule ccontr)
      assume "x  interior S"
      with x  R open R obtain y where "y  R - S"
        unfolding interior_def by fast
      from open R closed S have "open (R - S)"
        by (rule open_Diff)
      from R  S  T have "R - S  T"
        by fast
      from y  R - S open (R - S) R - S  T interior T = {} show False
        unfolding interior_def by fast
    qed
  qed
qed

lemma interior_Times: "interior (A × B) = interior A × interior B"
proof (rule interior_unique)
  show "interior A × interior B  A × B"
    by (intro Sigma_mono interior_subset)
  show "open (interior A × interior B)"
    by (intro open_Times open_interior)
  fix T
  assume "T  A × B" and "open T"
  then show "T  interior A × interior B"
  proof safe
    fix x y
    assume "(x, y)  T"
    then obtain C D where "open C" "open D" "C × D  T" "x  C" "y  D"
      using open T unfolding open_prod_def by fast
    then have "open C" "open D" "C  A" "D  B" "x  C" "y  D"
      using T  A × B by auto
    then show "x  interior A" and "y  interior B"
      by (auto intro: interiorI)
  qed
qed

lemma interior_Ici:
  fixes x :: "'a :: {dense_linorder,linorder_topology}"
  assumes "b < x"
  shows "interior {x ..} = {x <..}"
proof (rule interior_unique)
  fix T
  assume "T  {x ..}" "open T"
  moreover have "x  T"
  proof
    assume "x  T"
    obtain y where "y < x" "{y <.. x}  T"
      using open_left[OF open T x  T b < x] by auto
    with dense[OF y < x] obtain z where "z  T" "z < x"
      by (auto simp: subset_eq Ball_def)
    with T  {x ..} show False by auto
  qed
  ultimately show "T  {x <..}"
    by (auto simp: subset_eq less_le)
qed auto

lemma interior_Iic:
  fixes x :: "'a ::{dense_linorder,linorder_topology}"
  assumes "x < b"
  shows "interior {.. x} = {..< x}"
proof (rule interior_unique)
  fix T
  assume "T  {.. x}" "open T"
  moreover have "x  T"
  proof
    assume "x  T"
    obtain y where "x < y" "{x ..< y}  T"
      using open_right[OF open T x  T x < b] by auto
    with dense[OF x < y] obtain z where "z  T" "x < z"
      by (auto simp: subset_eq Ball_def less_le)
    with T  {.. x} show False by auto
  qed
  ultimately show "T  {..< x}"
    by (auto simp: subset_eq less_le)
qed auto

lemma countable_disjoint_nonempty_interior_subsets:
  fixes  :: "'a::second_countable_topology set set"
  assumes pw: "pairwise disjnt " and int: "S. S  ; interior S = {}  S = {}"
  shows "countable "
proof (rule countable_image_inj_on)
  have "disjoint (interior ` )"
    using pw by (simp add: disjoint_image_subset interior_subset)
  then show "countable (interior ` )"
    by (auto intro: countable_disjoint_open_subsets)
  show "inj_on interior "
    using pw apply (clarsimp simp: inj_on_def pairwise_def)
    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
    done
qed

subsection Closure of a Set

definitiontag important closure :: "('a::topological_space) set  'a set" where
"closure S = S  {x . x islimpt S}"

lemma interior_closure: "interior S = - (closure (- S))"
  by (auto simp: interior_def closure_def islimpt_def)

lemma closure_interior: "closure S = - interior (- S)"
  by (simp add: interior_closure)

lemma closed_closure[simp, intro]: "closed (closure S)"
  by (simp add: closure_interior closed_Compl)

lemma closure_subset: "S  closure S"
  by (simp add: closure_def)

lemma closure_hull: "closure S = closed hull S"
  by (auto simp: hull_def closure_interior interior_def)

lemma closure_eq: "closure S = S  closed S"
  unfolding closure_hull using closed_Inter by (rule hull_eq)

lemma closure_closed [simp]: "closed S  closure S = S"
  by (simp only: closure_eq)

lemma closure_closure [simp]: "closure (closure S) = closure S"
  unfolding closure_hull by (rule hull_hull)

lemma closure_mono: "S  T  closure S  closure T"
  unfolding closure_hull by (rule hull_mono)

lemma closure_minimal: "S  T  closed T  closure S  T"
  unfolding closure_hull by (rule hull_minimal)

lemma closure_unique:
  assumes "S  T"
    and "closed T"
    and "T'. S  T'  closed T'  T  T'"
  shows "closure S = T"
  using assms unfolding closure_hull by (rule hull_unique)

lemma closure_empty [simp]: "closure {} = {}"
  using closed_empty by (rule closure_closed)

lemma closure_UNIV [simp]: "closure UNIV = UNIV"
  using closed_UNIV by (rule closure_closed)

lemma closure_Un [simp]: "closure (S  T) = closure S  closure T"
  by (simp add: closure_interior)

lemma closure_eq_empty [iff]: "closure S = {}  S = {}"
  using closure_empty closure_subset[of S] by blast

lemma closure_subset_eq: "closure S  S  closed S"
  using closure_eq[of S] closure_subset[of S] by simp

lemma open_Int_closure_eq_empty: "open S  (S  closure T) = {}  S  T = {}"
  using open_subset_interior[of S "- T"]
  using interior_subset[of "- T"]
  by (auto simp: closure_interior)

lemma open_Int_closure_subset: "open S  S  closure T  closure (S  T)"
proof
  fix x
  assume *: "open S" "x  S  closure T"
  have "x islimpt (S  T)" if **: "x islimpt T"
  proof (rule islimptI)
    fix A
    assume "x  A" "open A"
    with * have "x  A  S" "open (A  S)"
      by (simp_all add: open_Int)
    with ** obtain y where "y  T" "y  A  S" "y  x"
      by (rule islimptE)
    then have "y  S  T" "y  A  y  x"
      by simp_all
    then show "y(S  T). y  A  y  x" ..
  qed
  with * show "x  closure (S  T)"
    unfolding closure_def by blast
qed

lemma closure_complement: "closure (- S) = - interior S"
  by (simp add: closure_interior)

lemma interior_complement: "interior (- S) = - closure S"
  by (simp add: closure_interior)

lemma interior_diff: "interior(S - T) = interior S - closure T"
  by (simp add: Diff_eq interior_complement)

lemma closure_Times: "closure (A × B) = closure A × closure B"
proof (rule closure_unique)
  show "A × B  closure A × closure B"
    by (intro Sigma_mono closure_subset)
  show "closed (closure A × closure B)"
    by (intro closed_Times closed_closure)
  fix T
  assume "A × B  T" and "closed T"
  then show "closure A × closure B  T"
    apply (simp add: closed_def open_prod_def, clarify)
    apply (rule ccontr)
    apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
    apply (simp add: closure_interior interior_def)
    apply (drule_tac x=C in spec)
    apply (drule_tac x=D in spec, auto)
    done
qed

lemma closure_open_Int_superset:
  assumes "open S" "S  closure T"
  shows "closure(S  T) = closure S"
proof -
  have "closure S  closure(S  T)"
    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
  then show ?thesis
    by (simp add: closure_mono dual_order.antisym)
qed

lemma closure_Int: "closure (I)  {closure S |S. S  I}"
proof -
  {
    fix y
    assume "y  I"
    then have y: "S  I. y  S" by auto
    {
      fix S
      assume "S  I"
      then have "y  closure S"
        using closure_subset y by auto
    }
    then have "y  {closure S |S. S  I}"
      by auto
  }
  then have "I  {closure S |S. S  I}"
    by auto
  moreover have "closed ({closure S |S. S  I})"
    unfolding closed_Inter closed_closure by auto
  ultimately show ?thesis using closure_hull[of "I"]
    hull_minimal[of "I" "{closure S |S. S  I}" "closed"] by auto
qed

lemma islimpt_in_closure: "(x islimpt S) = (xclosure(S-{x}))"
  unfolding closure_def using islimpt_punctured by blast

lemma connected_imp_connected_closure: "connected S  connected (closure S)"
  by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)

lemma bdd_below_closure:
  fixes A :: "real set"
  assumes "bdd_below A"
  shows "bdd_below (closure A)"
proof -
  from assms obtain m where "x. x  A  m  x"
    by (auto simp: bdd_below_def)
  then have "A  {m..}" by auto
  then have "closure A  {m..}"
    using closed_real_atLeast by (rule closure_minimal)
  then show ?thesis
    by (auto simp: bdd_below_def)
qed


subsection Frontier (also known as boundary)

definitiontag important frontier :: "('a::topological_space) set  'a set" where
"frontier S = closure S - interior S"

lemma frontier_closed [iff]: "closed (frontier S)"
  by (simp add: frontier_def closed_Diff)

lemma frontier_closures: "frontier S = closure S  closure (- S)"
  by (auto simp: frontier_def interior_closure)

lemma frontier_Int: "frontier(S  T) = closure(S  T)  (frontier S  frontier T)"
proof -
  have "closure (S  T)  closure S" "closure (S  T)  closure T"
    by (simp_all add: closure_mono)
  then show ?thesis
    by (auto simp: frontier_closures)
qed

lemma frontier_Int_subset: "frontier(S  T)  frontier S  frontier T"
  by (auto simp: frontier_Int)

lemma frontier_Int_closed:
  assumes "closed S" "closed T"
  shows "frontier(S  T) = (frontier S  T)  (S  frontier T)"
proof -
  have "closure (S  T) = T  S"
    using assms by (simp add: Int_commute closed_Int)
  moreover have "T  (closure S  closure (- S)) = frontier S  T"
    by (simp add: Int_commute frontier_closures)
  ultimately show ?thesis
    by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
qed

lemma frontier_subset_closed: "closed S  frontier S  S"
  by (metis frontier_def closure_closed Diff_subset)

lemma frontier_empty [simp]: "frontier {} = {}"
  by (simp add: frontier_def)

lemma frontier_subset_eq: "frontier S  S  closed S"
proof -
  {
    assume "frontier S  S"
    then have "closure S  S"
      using interior_subset unfolding frontier_def by auto
    then have "closed S"
      using closure_subset_eq by auto
  }
  then show ?thesis using frontier_subset_closed[of S] ..
qed

lemma frontier_complement [simp]: "frontier (- S) = frontier S"
  by (auto simp: frontier_def closure_complement interior_complement)

lemma frontier_Un_subset: "frontier(S  T)  frontier S  frontier T"
  by (metis compl_sup frontier_Int_subset frontier_complement)

lemma frontier_disjoint_eq: "frontier S  S = {}  open S"
  using frontier_complement frontier_subset_eq[of "- S"]
  unfolding open_closed by auto

lemma frontier_UNIV [simp]: "frontier UNIV = {}"
  using frontier_complement frontier_empty by fastforce

lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
  by (simp add: Int_commute frontier_def interior_closure)

lemma frontier_interior_subset: "frontier(interior S)  frontier S"
  by (simp add: Diff_mono frontier_interiors interior_mono interior_subset)

lemma closure_Un_frontier: "closure S = S  frontier S"
proof -
  have "S  interior S = S"
    using interior_subset by auto
  then show ?thesis
    using closure_subset by (auto simp: frontier_def)
qed


subsectiontag unimportant Filters and the ``eventually true'' quantifier

text Identify Trivial limits, where we can't approach arbitrarily closely.

lemma trivial_limit_within: "trivial_limit (at a within S)  ¬ a islimpt S"
proof
  assume "trivial_limit (at a within S)"
  then show "¬ a islimpt S"
    unfolding trivial_limit_def
    unfolding eventually_at_topological
    unfolding islimpt_def
    apply (clarsimp simp add: set_eq_iff)
    apply (rename_tac T, rule_tac x=T in exI)
    apply (clarsimp, drule_tac x=y in bspec, simp_all)
    done
next
  assume "¬ a islimpt S"
  then show "trivial_limit (at a within S)"
    unfolding trivial_limit_def eventually_at_topological islimpt_def
    by metis
qed

lemma trivial_limit_at_iff: "trivial_limit (at a)  ¬ a islimpt UNIV"
  using trivial_limit_within [of a UNIV] by simp

lemma trivial_limit_at: "¬ trivial_limit (at a)"
  for a :: "'a::perfect_space"
  by (rule at_neq_bot)

lemma not_trivial_limit_within: "¬ trivial_limit (at x within S) = (x  closure (S - {x}))"
  using islimpt_in_closure by (metis trivial_limit_within)

lemma not_in_closure_trivial_limitI:
  "x  closure s  trivial_limit (at x within s)"
  using not_trivial_limit_within[of x s]
  by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)

lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
  if "x  closure s  filterlim f l (at x within s)"
  by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)

lemma at_within_eq_bot_iff: "at c within A = bot  c  closure (A - {c})"
  using not_trivial_limit_within[of c A] by blast

text Some property holds "sufficiently close" to the limit point.

lemma trivial_limit_eventually: "trivial_limit net  eventually P net"
  by simp

lemma trivial_limit_eq: "trivial_limit net  (P. eventually P net)"
  by (simp add: filter_eq_iff)

lemma Lim_topological:
  "(f  l) net 
    trivial_limit net  (S. open S  l  S  eventually (λx. f x  S) net)"
  unfolding tendsto_def trivial_limit_eq by auto

lemma eventually_within_Un:
  "eventually P (at x within (s  t)) 
    eventually P (at x within s)  eventually P (at x within t)"
  unfolding eventually_at_filter
  by (auto elim!: eventually_rev_mp)

lemma Lim_within_union:
 "(f  l) (at x within (s  t)) 
  (f  l) (at x within s)  (f  l) (at x within t)"
  unfolding tendsto_def
  by (auto simp: eventually_within_Un)


subsection Limits

text The expected monotonicity property.

lemma Lim_Un:
  assumes "(f  l) (at x within S)" "(f  l) (at x within T)"
  shows "(f  l) (at x within (S  T))"
  using assms unfolding at_within_union by (rule filterlim_sup)

lemma Lim_Un_univ:
  "(f  l) (at x within S)  (f  l) (at x within T) 
    S  T = UNIV  (f  l) (at x)"
  by (metis Lim_Un)

text Interrelations between restricted and unrestricted limits.

lemma Lim_at_imp_Lim_at_within: "(f  l) (at x)  (f  l) (at x within S)"
  by (metis order_refl filterlim_mono subset_UNIV at_le)

lemma eventually_within_interior:
  assumes "x  interior S"
  shows "eventually P (at x within S)  eventually P (at x)"
  (is "?lhs = ?rhs")
proof
  from assms obtain T where T: "open T" "x  T" "T  S" ..
  {
    assume ?lhs
    then obtain A where "open A" and "x  A" and "yA. y  x  y  S  P y"
      by (auto simp: eventually_at_topological)
    with T have "open (A  T)" and "x  A  T" and "y  A  T. y  x  P y"
      by auto
    then show ?rhs
      by (auto simp: eventually_at_topological)
  next
    assume ?rhs
    then show ?lhs
      by (auto elim: eventually_mono simp: eventually_at_filter)
  }
qed

lemma at_within_interior: "x  interior S  at x within S = at x"
  unfolding filter_eq_iff by (intro allI eventually_within_interior)

lemma Lim_within_LIMSEQ:
  fixes a :: "'a::first_countable_topology"
  assumes "S. (n. S n  a  S n  T)  S  a  (λn. X (S n))  L"
  shows "(X  L) (at a within T)"
  using assms unfolding tendsto_def [where l=L]
  by (simp add: sequentially_imp_eventually_within)

lemma Lim_right_bound:
  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} 
    'b::{linorder_topology, conditionally_complete_linorder}"
  assumes mono: "a b. a  I  b  I  x < a  a  b  f a  f b"
    and bnd: "a. a  I  x < a  K  f a"
  shows "(f  Inf (f ` ({x<..}  I))) (at x within ({x<..}  I))"
proof (cases "{x<..}  I = {}")
  case True
  then show ?thesis by simp
next
  case False
  show ?thesis
  proof (rule order_tendstoI)
    fix a
    assume a: "a < Inf (f ` ({x<..}  I))"
    {
      fix y
      assume "y  {x<..}  I"
      with False bnd have "Inf (f ` ({x<..}  I))  f y"
        by (auto intro!: cInf_lower bdd_belowI2)
      with a have "a < f y"
        by (blast intro: less_le_trans)
    }
    then show "eventually (λx. a < f x) (at x within ({x<..}  I))"
      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
  next
    fix a
    assume "Inf (f ` ({x<..}  I)) < a"
    from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y  I" "f y < a"
      by auto
    then have "eventually (λx. x  I  f x < a) (at_right x)"
      unfolding eventually_at_right[OF x < y] by (metis less_imp_le le_less_trans mono)
    then show "eventually (λx. f x < a) (at x within ({x<..}  I))"
      unfolding eventually_at_filter by eventually_elim simp
  qed
qed

(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
lemma islimpt_sequential:
  fixes x :: "'a::first_countable_topology"
  shows "x islimpt S  (f. (n::nat. f n  S - {x})  (f  x) sequentially)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  from countable_basis_at_decseq[of x] obtain A where A:
      "i. open (A i)"
      "i. x  A i"
      "S. open S  x  S  eventually (λi. A i  S) sequentially"
    by blast
  define f where "f n = (SOME y. y  S  y  A n  x  y)" for n
  {
    fix n
    from ?lhs have "y. y  S  y  A n  x  y"
      unfolding islimpt_def using A(1,2)[of n] by auto
    then have "f n  S  f n  A n  x  f n"
      unfolding f_def by (rule someI_ex)
    then have "f n  S" "f n  A n" "x  f n" by auto
  }
  then have "n. f n  S - {x}" by auto
  moreover have "(λn. f n)  x"
  proof (rule topological_tendstoI)
    fix S
    assume "open S" "x  S"
    from A(3)[OF this] n. f n  A n
    show "eventually (λx. f x  S) sequentially"
      by (auto elim!: eventually_mono)
  qed
  ultimately show ?rhs by fast
next
  assume ?rhs
  then obtain f :: "nat  'a" where f: "n. f n  S - {x}" and lim: "f  x"
    by auto
  show ?lhs
    unfolding islimpt_def
  proof safe
    fix T
    assume "open T" "x  T"
    from lim[THEN topological_tendstoD, OF this] f
    show "yS. y  T  y  x"
      unfolding eventually_sequentially by auto
  qed
qed

textThese are special for limits out of the same topological space.

lemma Lim_within_id: "(id  a) (at a within s)"
  unfolding id_def by (rule tendsto_ident_at)

lemma Lim_at_id: "(id  a) (at a)"
  unfolding id_def by (rule tendsto_ident_at)

textIt's also sometimes useful to extract the limit point from the filter.

abbreviation netlimit :: "'a::t2_space filter  'a"
  where "netlimit F  Lim F (λx. x)"

lemma netlimit_at [simp]:
  fixes a :: "'a::{perfect_space,t2_space}"
  shows "netlimit (at a) = a"
  using Lim_ident_at [of a UNIV] by simp

lemma lim_within_interior:
  "x  interior S  (f  l) (at x within S)  (f  l) (at x)"
  by (metis at_within_interior)

lemma netlimit_within_interior:
  fixes x :: "'a::{t2_space,perfect_space}"
  assumes "x  interior S"
  shows "netlimit (at x within S) = x"
  using assms by (metis at_within_interior netlimit_at)

textUseful lemmas on closure and set of possible sequential limits.

lemma closure_sequential:
  fixes l :: "'a::first_countable_topology"
  shows "l  closure S  (x. (n. x n  S)  (x  l) sequentially)"
  (is "?lhs = ?rhs")
proof
  assume "?lhs"
  moreover
  {
    assume "l  S"
    then have "?rhs" using tendsto_const[of l sequentially] by auto
  }
  moreover
  {
    assume "l islimpt S"
    then have "?rhs" unfolding islimpt_sequential by auto
  }
  ultimately show "?rhs"
    unfolding closure_def by auto
next
  assume "?rhs"
  then show "?lhs" unfolding closure_def islimpt_sequential by auto
qed

lemma closed_sequential_limits:
  fixes S :: "'a::first_countable_topology set"
  shows "closed S  (x l. (n. x n  S)  (x  l) sequentially  l  S)"
by (metis closure_sequential closure_subset_eq subset_iff)

lemma tendsto_If_within_closures:
  assumes f: "x  s  (closure s  closure t) 
      (f  l x) (at x within s  (closure s  closure t))"
  assumes g: "x  t  (closure s  closure t) 
      (g  l x) (at x within t  (closure s  closure t))"
  assumes "x  s  t"
  shows "((λx. if x  s then f x else g x)  l x) (at x within s  t)"
proof -
  have *: "(s  t)  {x. x  s} = s" "(s  t)  {x. x  s} = t - s"
    by auto
  have "(f  l x) (at x within s)"
    by (rule filterlim_at_within_closure_implies_filterlim)
       (use x  _ in auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f])
  moreover
  have "(g  l x) (at x within t - s)"
    by (rule filterlim_at_within_closure_implies_filterlim)
      (use x  _ in
        auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset)
  ultimately show ?thesis
    by (intro filterlim_at_within_If) (simp_all only: *)
qed


subsection Compactness

lemma brouwer_compactness_lemma:
  fixes f :: "'a::topological_space  'b::real_normed_vector"
  assumes "compact s"
    and "continuous_on s f"
    and "¬ (xs. f x = 0)"
  obtains d where "0 < d" and "xs. d  norm (f x)"
proof (cases "s = {}")
  case True
  show thesis
    by (rule that [of 1]) (auto simp: True)
next
  case False
  have "continuous_on s (norm  f)"
    by (rule continuous_intros continuous_on_norm assms(2))+
  with False obtain x where x: "x  s" "ys. (norm  f) x  (norm  f) y"
    using continuous_attains_inf[OF assms(1), of "norm  f"]
    unfolding o_def
    by auto
  have "(norm  f) x > 0"
    using assms(3) and x(1)
    by auto
  then show ?thesis
    by (rule that) (insert x(2), auto simp: o_def)
qed

subsubsection Bolzano-Weierstrass property

proposition Heine_Borel_imp_Bolzano_Weierstrass:
  assumes "compact s"
    and "infinite t"
    and "t  s"
  shows "x  s. x islimpt t"
proof (rule ccontr)
  assume "¬ (x  s. x islimpt t)"
  then obtain f where f: "xs. x  f x  open (f x)  (yt. y  f x  y = x)"
    unfolding islimpt_def
    using bchoice[of s "λ x T. x  T  open T  (yt. y  T  y = x)"]
    by auto
  obtain g where g: "g  {t. x. x  s  t = f x}" "finite g" "s  g"
    using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. x. xs  t = f x}"]]
    using f by auto
  from g(1,3) have g':"xg. xa  s. x = f xa"
    by auto
  {
    fix x y
    assume "x  t" "y  t" "f x = f y"
    then have "x  f x"  "y  f x  y = x"
      using f[THEN bspec[where x=x]] and t  s by auto
    then have "x = y"
      using f x = f y and f[THEN bspec[where x=y]] and y  t and t  s
      by auto
  }
  then have "inj_on f t"
    unfolding inj_on_def by simp
  then have "infinite (f ` t)"
    using assms(2) using finite_imageD by auto
  moreover
  {
    fix x
    assume "x  t" "f x  g"
    from g(3) assms(3) x  t obtain h where