Theory HOL-Analysis.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))"
    (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (meson local.open_Union subsetD topological_basis_def)
  show "?rhs  ?lhs"
    unfolding topological_basis_def
    by (metis cSup_singleton empty_subsetI insert_subset)
qed

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"
  by (simp add: assms topological_basis_iff)

lemma topological_basisE:
  fixes O'
  assumes "topological_basis B"
    and "open O'"
    and "x  O'"
  obtains B' where "B'  B" "x  B'" "B'  O'"
  by (metis assms topological_basis_def topological_basis_iff)

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 "B'. B'  {}  f B'  B'"
  shows "X. open X  X  {}  (B'  B. f B'  X)"
  by (metis assms equals0D in_mono topological_basisE)

end

lemma topological_basis_prod:
  assumes A: "topological_basis A"
    and B: "topological_basis B"
  shows "topological_basis ((λ(a, b). a × b) ` (A × B))"
proof -
  have "XA × B. ((a,b)X. a × b) = S" if "open S" for S
  proof -
    have "(x, y)  ((a, b){X  A × B. fst X × snd X  S}. a × b)"
      if xy: "(x, y)  S" for x y
    proof -
      obtain a b where a: "open a""x  a" and b: "open b" "y  b" and "a × b  S"
        by (metis open_prod_elim[OF open S] xy mem_Sigma_iff)
      moreover obtain A0 where "A0  A" "x  A0" "A0  a"
        using A a b topological_basisE by blast
      moreover
      from B b obtain B0 where "B0  B" "y  B0" "B0  b"
        by (rule topological_basisE)
      ultimately show ?thesis
        by (intro UN_I[of "(A0, B0)"]) auto
    qed
    then have "((a, b){x  A × B. fst x × snd x  S}. a × b) = S"
      by force
    then show ?thesis
      using subset_eq by force
  qed
  with A B show ?thesis
    unfolding topological_basis_def
    by (smt (verit) SigmaE imageE image_mono open_Times case_prod_conv)
qed


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 auto

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
  moreover have "countable (range 𝒜)"
    by simp
  ultimately show thesis
    by (smt (verit, best) imageE rangeI that)
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
    moreover have "a𝒜"
      unfolding 𝒜_def 
    proof (rule image_eqI)
      show "a =  (from_nat_into  ` {to_nat_on  a})"
        by (simp add:  a)
    qed auto
    ultimately show "a𝒜. a  S"
      by blast 
  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" 
  then show "i. from_nat_into 𝒜 i  S"
    by (metis "2" countable 𝒜 from_nat_into_surj)
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
    obtain a b where "a  𝒜" "a  a'" "b  B" "b  b'"
      by (meson B(4) 𝒜(4) a'b' mem_Times_iff)
    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 𝒟"
    by (simp add: 𝒟_def countable )
  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: " = 𝒟" ..
  moreover have "𝒟 =  (G ` 𝒟)"
    using G eq1 by auto
  ultimately show ?thesis
    by (metis G countable 𝒟 countable_image image_subset_iff that)
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 open_subopen [of "-S"]
  by (metis Compl_iff islimptE islimptI open_subopen subsetI)

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_finite_union_iff:
  assumes "finite A"
  shows   "z islimpt (xA. B x)  (xA. z islimpt B x)"
  using assms by (induction rule: finite_induct) (simp_all add: islimpt_Un)

lemma islimpt_insert:
  fixes x :: "'a::t1_space"
  shows "x islimpt (insert a S)  x islimpt S"
proof
  assume "x islimpt (insert a S)"
  then show "x islimpt S"
    by (metis closed_limpt closed_singleton empty_iff insert_iff insert_is_Un islimpt_Un islimpt_def)
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 "x. x  (T  S - {l})"
    by (metis ex_in_conv finite.emptyI infinite_remove)
  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}"
      by (metis all_not_in_conv finite.emptyI)
    then have "a. i < a  f a  A (Suc n)"
      by (force simp: linorder_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: "(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
  then obtain N where "nN. f n  t"
    by (meson f lim_explicit)

  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 s  t = {} show False
    by blast
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

lemma islimpt_isCont_image:
  fixes f :: "'a :: {first_countable_topology, t2_space}  'b :: {first_countable_topology, t2_space}"
  assumes "x islimpt A" and "isCont f x" and ev: "eventually (λy. f y  f x) (at x)"
  shows   "f x islimpt f ` A"
proof -
  from assms(1) obtain g where g: "g  x" "range g  A - {x}"
    unfolding islimpt_sequential by blast
  have "filterlim g (at x) sequentially"
    using g by (auto simp: filterlim_at intro!: always_eventually)
  then obtain N where N: "n. n  N  f (g n)  f x"
    by (metis (mono_tags, lifting) ev eventually_at_top_linorder filterlim_iff)
  have "(λx. g (x + N))  x"
    using g(1) by (rule LIMSEQ_ignore_initial_segment)
  hence "(λx. f (g (x + N)))  f x"
    using assms(2) isCont_tendsto_compose by blast
  moreover have "range (λx. f (g (x + N)))  f ` A - {f x}"
    using g(2) N by auto
  ultimately show ?thesis
    unfolding islimpt_sequential by (intro exI[of _ "λx. f (g (x + N))"]) auto
qed

lemma islimpt_image:
  assumes "z islimpt g -` A  B" "g z  A" "z  B" "continuous_on B g"
  shows   "g z islimpt A"
  by (smt (verit, best) IntD1 assms continuous_on_topological inf_le2 islimpt_def subset_eq vimageE)
  

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"
proof -
  obtain T where "x  T" "T  S" "open T"
    using interior_subset x by blast
  with x islimpt_UNIV [of x]  show ?thesis
    unfolding islimpt_def by (metis (full_types) Int_iff open_Int subsetD)
qed

lemma open_imp_islimpt:
  fixes x::"'a:: perfect_space"
  assumes "open S" "xS"
  shows "x islimpt S"
  using assms interior_eq interior_limit_point by auto

lemma islimpt_Int_eventually:
  assumes "x islimpt A" "eventually (λy. y  B) (at x)"
  shows   "x islimpt A  B"
  using assms unfolding islimpt_def eventually_at_filter eventually_nhds
  by (metis Int_iff UNIV_I open_Int)

lemma islimpt_conv_frequently_at:
  "x islimpt A  frequently (λy. y  A) (at x)"
  by (simp add: frequently_def islimpt_iff_eventually)

lemma frequently_at_imp_islimpt:
  assumes "frequently (λy. y  A) (at x)"
  shows   "x islimpt A"
  by (simp add: assms islimpt_conv_frequently_at)  

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
      then show False
        by (metis Diff_subset_conv R  S  T open R cS empty_iff iT interiorI open_Diff)
    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"
  then have "x islimpt (S  T)" if "x islimpt T"
    by (metis IntD1 eventually_at_in_open' inf_commute islimpt_Int_eventually that)
  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"
  by (metis Int_Un_distrib Un_Int_eq(4) assms closure_Un closure_closure open_Int_closure_subset sup.orderE)

lemma closure_Int: "closure (I)  {closure S |S. S  I}"
  by (simp add: INF_greatest Inter_lower Setcompr_eq_image closure_mono)

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)"
  by (smt (verit, best) Diff_Int Int_Diff assms closed_Int closure_eq frontier_def inf_commute interior_Int)

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"
  by (metis Diff_subset_conv closure_subset_eq frontier_def interior_subset subset_Un_eq)

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"
  by (simp add: closure_def frontier_closures sup_inf_distrib1)


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"
    unfolding trivial_limit_def eventually_at_topological islimpt_def
    by blast

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_iff_le_filtercomap 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

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)"
  by (metis assms at_within_open_subset interior_subset open_interior)

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

text‹These 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)

text‹It'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)

text‹Useful 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)"
  by (metis Diff_empty Diff_insert0 Un_iff closure_def islimpt_sequential mem_Collect_eq tendsto_const)

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
  then show ?thesis
    by (metis assms(3) that comp_apply zero_less_norm_iff)
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 by metis
  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
  then have g': "xg. y  S. x = f y"
    by auto
  have "inj_on f T"
    by (smt (verit, best) assms(3) f inj_onI subsetD)
  then have "infinite (f ` T)"
    using assms(2) using finite_imageD by auto
  moreover
    have False if "x  T" "f x  g" for x
      by (smt (verit) UnionE assms(3) f g' g(3) subsetD that)
  then have "f ` T  g" by auto
  ultimately show False
    using g(2) using finite_subset by auto
qed

lemma sequence_infinite_lemma:
  fixes f :: "nat  'a::t1_space"
  assumes "n. f n  l"
    and "(f  l) sequentially"
  shows "infinite (range f)"
proof
  assume "finite (range f)"
  then have "l  range f  closed (range f)"
    using finite (range f) assms(1) finite_imp_closed by blast
  then have "eventually (λn. f n  - range f) sequentially"
    by (metis Compl_iff assms(2) open_Compl topological_tendstoD)
  then show False
    unfolding eventually_sequentially by auto
qed

lemma Bolzano_Weierstrass_imp_closed:
  fixes S :: "'a::{first_countable_topology,t2_space} set"
  assumes "T. infinite T  T  S --> (x  S. x islimpt T)"
  shows "closed S"
proof -
  {
    fix x l
    assume as: "n::nat. x n  S" "(x  l) sequentially"
    have "l  S"
    proof (cases "n. x n  l")
      case False
      then show "lS" using as(1) by auto
    next
      case True
      with as(2) have "infinite (range x)"
        using sequence_infinite_lemma[of x l] by auto
      then obtain l' where "l'S" "l' islimpt (range x)"
        using as(1) assms by auto
      then show "lS" using sequence_unique_limpt as True by auto
    qed
  }
  then show ?thesis
    unfolding closed_sequential_limits by fast
qed

lemma closure_insert:
  fixes x :: "'a::t1_space"
  shows "closure (insert x S) = insert x (closure S)"
  by (metis closed_singleton closure_Un closure_closed insert_is_Un)

lemma finite_not_islimpt_in_compact:
  assumes "compact A" "z. z  A  ¬z islimpt B"
  shows   "finite (A  B)"
  by (meson Heine_Borel_imp_Bolzano_Weierstrass assms inf_le1 inf_le2 islimpt_subset)


text‹In particular, some common special cases.›

lemma compact_Un [intro]:
  assumes "compact S"
    and "compact T"
  shows " compact (S  T)"
proof (rule compactI)
  fix f
  assume *: "Ball f open" "S  T  f"
  from * compact S obtain s' where "s'  f  finite s'  S  s'"
    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
  moreover
  from * compact T obtain t' where "t'  f  finite t'  T  t'"
    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
  ultimately show "f'f. finite f'  S  T  f'"
    by (auto intro!: exI[of _ "s'  t'"])
qed

lemma compact_Union [intro]: "finite S  (T. T  S  compact T)  compact (S)"
  by (induct set: finite) auto

lemma compact_UN [intro]:
  "finite A  (x. x  A  compact (B x))  compact (xA. B x)"
  by blast

lemma closed_Int_compact [intro]:
  assumes "closed S" and "compact T"
  shows "compact (S  T)"
  using compact_Int_closed [of T S] assms
  by (simp add: Int_commute)

lemma compact_Int [intro]:
  fixes S T :: "'a :: t2_space set"
  assumes "compact S" and "compact T"
  shows "compact (S  T)"
  using assms by (intro compact_Int_closed compact_imp_closed)

lemma compact_sing [simp]: "compact {a}"
  unfolding compact_eq_Heine_Borel by auto

lemma compact_insert [simp]:
  assumes "compact S"
  shows "compact (insert x S)"
  by (metis assms compact_Un compact_sing insert_is_Un)

lemma finite_imp_compact: "finite S  compact S"
  by (induct set: finite) simp_all

lemma open_delete:
  fixes S :: "'a::t1_space set"
  shows "open S  open (S - {x})"
  by (simp add: open_Diff)


text‹Compactness expressed with filters›

lemma closure_iff_nhds_not_empty:
  "x  closure X  (A. SA. open S  x  S  X  A  {})"
proof safe
  assume x: "x  closure X"
  fix S A
  assume §: "open S" "x  S" "X  A = {}" "S  A"
  then have "x  closure (-S)"
    by (simp add: closed_open)
  with x have "x  closure X - closure (-S)"
    by auto
  with § show False
    by (metis Compl_iff Diff_iff closure_mono disjoint_iff subsetD subsetI)
next
  assume "A S. S  A  open S  x  S  X  A  {}"
  then show "x  closure X"
    by (metis ComplI Compl_disjoint closure_interior interior_subset open_interior)
qed

lemma compact_filter:
  "compact U  (F. F  bot  eventually (λx. x  U) F  (xU. inf (nhds x) F  bot))"
proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
  fix F
  assume "compact U"
  assume F: "F  bot" "eventually (λx. x  U) F"
  then have "U  {}"
    by (auto simp: eventually_False)

  define Z where "Z = closure ` {A. eventually (λx. x  A) F}"
  then have "zZ. closed z"
    by auto
  moreover
  have ev_Z: "z. z  Z  eventually (λx. x  z) F"
    unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
  have "(B  Z. finite B  U  B  {})"
  proof (intro allI impI)
    fix B assume "finite B" "B  Z"
    with finite B ev_Z F(2) have "eventually (λx. x  U  (B)) F"
      by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
    with F show "U  B  {}"
      by (intro notI) (simp add: eventually_False)
  qed
  ultimately have "U  Z  {}"
    using compact U unfolding compact_fip by blast
  then obtain x where "x  U" and x: "z. z  Z  x  z"
    by auto

  have "P. eventually P (inf (nhds x) F)  P  bot"
    unfolding eventually_inf eventually_nhds
  proof safe
    fix P Q R S
    assume "eventually R F" "open S" "x  S"
    with open_Int_closure_eq_empty[of S "{x. R x}"] x
    have "S  {x. R x}  {}" by (auto simp: Z_def)
    moreover assume "Ball S Q" "x. Q x  R x  bot x"
    ultimately show False by (auto simp: set_eq_iff)
  qed
  with x  U show "xU. inf (nhds x) F  bot"
    by (metis eventually_bot)
next
  fix A
  assume A: "aA. closed a" "BA. finite B  U  B  {}" "U  A = {}"
  define F where "F = (INF ainsert U A. principal a)"
  have "F  bot"
    unfolding F_def
  proof (rule INF_filter_not_bot)
    fix X
    assume X: "X  insert U A" "finite X"
    with A(2)[THEN spec, of "X - {U}"] have "U  (X - {U})  {}"
      by auto
    with X show "(INF aX. principal a)  bot"
      by (auto simp: INF_principal_finite principal_eq_bot_iff)
  qed
  moreover
  have "F  principal U"
    unfolding F_def by auto
  then have "eventually (λx. x  U) F"
    by (auto simp: le_filter_def eventually_principal)
  moreover
  assume "F. F  bot  eventually (λx. x  U) F  (xU. inf (nhds x) F  bot)"
  ultimately obtain x where "x  U" and x: "inf (nhds x) F  bot"
    by auto

  { fix V assume "V  A"
    then have "F  principal V"
      unfolding F_def by (intro INF_lower2[of V]) auto
    then have V: "eventually (λx. x  V) F"
      by (auto simp: le_filter_def eventually_principal)
    have "x  closure V"
      unfolding closure_iff_nhds_not_empty
    proof (intro impI allI)
      fix S A
      assume "open S" "x  S" "S  A"
      then have "eventually (λx. x  A) (nhds x)"
        by (auto simp: eventually_nhds)
      with V have "eventually (λx. x  V  A) (inf (nhds x) F)"
        by (auto simp: eventually_inf)
      with x show "V  A  {}"
        by (auto simp del: Int_iff simp add: trivial_limit_def)
    qed
    then have "x  V"
      using V  A A(1) by simp
  }
  with xU have "x  U  A" by auto
  with U  A = {} show False by auto
qed

definitiontag important› countably_compact :: "('a::topological_space) set  bool" where
"countably_compact U 
  (A. countable A  (aA. open a)  U  A
      (TA. finite T  U  T))"

lemma countably_compactE:
  assumes "countably_compact s" and "tC. open t" and "s  C" "countable C"
  obtains C' where "C'  C" and "finite C'" and "s  C'"
  using assms unfolding countably_compact_def by metis

lemma countably_compactI:
  assumes "C. tC. open t  s  C  countable C  (C'C. finite C'  s  C')"
  shows "countably_compact s"
  using assms unfolding countably_compact_def by metis

lemma compact_imp_countably_compact: "compact U  countably_compact U"
  by (auto simp: compact_eq_Heine_Borel countably_compact_def)

lemma countably_compact_imp_compact:
  assumes "countably_compact U"
    and ccover: "countable B" "bB. open b"
    and basis: "T x. open T  x  T  x  U  bB. x  b  b  U  T"
  shows "compact U"
  using countably_compact U
  unfolding compact_eq_Heine_Borel countably_compact_def
proof safe
  fix A
  assume A: "aA. open a" "U  A"
  assume *: "A. countable A  (aA. open a)  U  A  (TA. finite T  U  T)"
  moreover define C where "C = {bB. aA. b  U  a}"
  ultimately have "countable C" "aC. open a"
    unfolding C_def using ccover by auto
  moreover
  have "A  U  C"
  proof safe
    fix x a
    assume "x  U" "x  a" "a  A"
    with basis[of a x] A obtain b where "b  B" "x  b" "b  U  a"
      by blast
    with a  A show "x  C"
      unfolding C_def by auto
  qed
  then have "U  C" using U  A by auto
  ultimately obtain T where T: "TC" "finite T" "U  T"
    using * by metis
  then have "tT. aA. t  U  a"
    by (auto simp: C_def)
  then obtain f where "tT. f t  A  t  U  f t"
    unfolding bchoice_iff Bex_def ..
  with T show "TA. finite T  U  T"
    unfolding C_def by (intro exI[of _ "f`T"]) fastforce
qed

proposition countably_compact_imp_compact_second_countable:
  "countably_compact U  compact (U :: 'a :: second_countable_topology set)"
proof (rule countably_compact_imp_compact)
  fix T and x :: 'a
  assume "open T" "x  T"
  from topological_basisE[OF is_basis this] obtain b where
    "b  (SOME B. countable B  topological_basis B)" "x  b" "b  T" .
  then show "bSOME B. countable B  topological_basis B. x  b  b  U  T"
    by blast
qed (insert countable_basis topological_basis_open[OF is_basis], auto)

lemma countably_compact_eq_compact:
  "countably_compact U  compact (U :: 'a :: second_countable_topology set)"
  using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast

subsubsection‹Sequential compactness›

definitiontag important› seq_compact :: "'a::topological_space set  bool" where
  "seq_compact S 
    (f. (n. f n  S)  (lS. r::natnat. strict_mono r  (f  r)  l))"

lemma seq_compactI:
  assumes "f. n. f n  S  lS. r::natnat. strict_mono r  (f  r)  l"
  shows "seq_compact S"
  unfolding seq_compact_def using assms by fast

lemma seq_compactE:
  assumes "seq_compact S" "n. f n  S"
  obtains l r where "l  S" "strict_mono (r :: nat  nat)" "(f  r)  l"
  using assms unfolding seq_compact_def by fast

lemma seq_compact_Int_closed:
  assumes "seq_compact S" and "closed T"
  shows "seq_compact (S  T)"
proof (rule seq_compactI)
  fix f assume "n::nat. f n  S  T"
  hence "n. f n  S" and "n. f n  T"
    by simp_all
  from seq_compact S and n. f n  S
  obtain l r where "l  S" and r: "strict_mono r" and l: "(f  r)  l"
    by (rule seq_compactE)
  from n. f n  T have "n. (f  r) n  T"
    by simp
  with l  S and r and l show "lS  T. r. strict_mono r  (f  r)  l"
    by (metis Int_iff closed T closed_sequentially)
qed

lemma seq_compact_closed_subset:
  assumes "closed S" and "S  T" and "seq_compact T"
  shows "seq_compact S"
  using assms seq_compact_Int_closed [of T S] by (simp add: Int_absorb1)

lemma seq_compact_imp_countably_compact:
  fixes U :: "'a :: first_countable_topology set"
  assumes "seq_compact U"
  shows "countably_compact U"
proof (safe intro!: countably_compactI)
  fix A
  assume A: "aA. open a" "U  A" "countable A"
  have subseq: "X. range X  U  r x. x  U  strict_mono (r :: nat  nat)  (X  r)  x"
    using seq_compact U by (fastforce simp: seq_compact_def subset_eq)
  show "TA. finite T  U  T"
  proof cases
    assume "finite A"
    with A show ?thesis by auto
  next
    assume "infinite A"
    then have "A  {}" by auto
    show ?thesis
    proof (rule ccontr)
      assume "¬ (TA. finite T  U  T)"
      then have "T. x. T  A  finite T  (x  U - T)"
        by auto
      then obtain X' where T: "T. T  A  finite T  X' T  U - T"
        by metis
      define X where "X n = X' (from_nat_into A ` {.. n})" for n
      have X: "n. X n  U - (in. from_nat_into A i)"
        using A  {} unfolding X_def by (intro T) (auto intro: from_nat_into)
      then have "range X  U"
        by auto
      with subseq[of X] obtain r x where "x  U" and r: "strict_mono r" "(X  r)  x"
        by auto
      from xU U  A from_nat_into_surj[OF countable A]
      obtain n where "x  from_nat_into A n" by auto
      with r(2) A(1) from_nat_into[OF A  {}]
      have "eventually (λi. X (r i)  from_nat_into A n) sequentially"
        unfolding tendsto_def by fastforce
      then obtain N where "i. N  i  X (r i)  from_nat_into A n"
        by (auto simp: eventually_sequentially)
      moreover from X have "i. n  r i  X (r i)  from_nat_into A n"
        by auto
      moreover from strict_mono r[THEN seq_suble, of "max n N"] have "i. n  r i  N  i"
        by (auto intro!: exI[of _ "max n N"])
      ultimately show False
        by auto
    qed
  qed
qed

lemma compact_imp_seq_compact:
  fixes U :: "'a :: first_countable_topology set"
  assumes "compact U"
  shows "seq_compact U"
  unfolding seq_compact_def
proof safe
  fix X :: "nat  'a"
  assume "n. X n  U"
  then have "eventually (λx. x  U) (filtermap X sequentially)"
    by (auto simp: eventually_filtermap)
  moreover
  have "filtermap X sequentially  bot"
    by (simp add: trivial_limit_def eventually_filtermap)
  ultimately
  obtain x where "x  U" and x: "inf (nhds x) (filtermap X sequentially)  bot" (is "?F  _")
    using compact U by (auto simp: compact_filter)

  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 s where "s n i = (SOME j. i < j  X j  A (Suc n))" for n i
  {
    fix n i
    have "a. i < a  X a  A (Suc n)"
    proof (rule ccontr)
      assume "¬ (a>i. X a  A (Suc n))"
      then have "a. Suc i  a  X a  A (Suc n)"
        by auto
      then have "eventually (λx. x  A (Suc n)) (filtermap X sequentially)"
        by (auto simp: eventually_filtermap eventually_sequentially)
      moreover have "eventually (λx. x  A (Suc n)) (nhds x)"
        using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds)
      ultimately have "eventually (λx. False) ?F"
        by (auto simp: eventually_inf)
      with x show False
        by (simp add: eventually_False)
    qed
    then have "i < s n i" "X (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. X (r n))  x"
  proof (rule topological_tendstoI)
    fix S
    assume "open S" "x  S"
    with A(3) have "eventually (λi. A i  S) sequentially"
      by auto
    moreover
    {
      fix i
      assume "Suc 0  i"
      then have "X (r i)  A i"
        by (cases i) (simp_all add: r_def s)
    }
    then have "eventually (λi. X (r i)  A i) sequentially"
      by (auto simp: eventually_sequentially)
    ultimately show "eventually (λi. X (r i)  S) sequentially"
      by eventually_elim auto
  qed
  ultimately show "x  U. r. strict_mono r  (X  r)  x"
    using x  U by (auto simp: convergent_def comp_def)
qed

lemma countably_compact_imp_acc_point:
  assumes "countably_compact S"
    and "countable T"
    and "infinite T"
    and "T  S"
  shows "xS. U. xU  open U  infinite (U  T)"
proof (rule ccontr)
  define C where "C = (λF. interior (F  (- T))) ` {F. finite F  F  T }"
  note countably_compact S
  moreover have "TC. open T"
    by (auto simp: C_def)
  moreover
  assume "¬ (xS. U. xU  open U  infinite (U  T))"
  then have S: "x. x  S  U. xU  open U  finite (U  T)" by metis
  have "S  C"
    using T  S
    unfolding C_def
    apply (safe dest!: S)
    apply (rule_tac a="U  T" in UN_I)
    apply (auto intro!: interiorI simp add: finite_subset)
    done
  moreover
  from countable T have "countable C"
    unfolding C_def by (auto intro: countable_Collect_finite_subset)
  ultimately
  obtain D where "D  C" "finite D" "S  D"
    by (rule countably_compactE)
  then obtain E where E: "E  {F. finite F  F  T }" "finite E"
    and S: "S  (FE. interior (F  (- T)))"
    by (metis (lifting) finite_subset_image C_def)
  from S T  S have "T  E"
    using interior_subset by blast
  moreover have "finite (E)"
    using E by auto
  ultimately show False using infinite T
    by (auto simp: finite_subset)
qed

lemma countable_acc_point_imp_seq_compact:
  fixes S :: "'a::first_countable_topology set"
  assumes "T. infinite T; countable T; T  S  xS. U. xU  open U  infinite (U  T)"
  shows "seq_compact S"
  unfolding seq_compact_def
proof (intro strip)
  fix f :: "nat  'a"
  assume f: "n. f n  S"
  show "lS. r. strict_mono r  ((f  r)  l) sequentially"
  proof (cases "finite (range f)")
    case True
    obtain l where "infinite {n. f n = f l}"
      using pigeonhole_infinite[OF _ True] by auto
    then obtain r :: "nat  nat" where "strict_mono  r" and fr: "n. f (r n) = f l"
      using infinite_enumerate by blast
    then have "strict_mono r  (f  r)  f l"
      by (simp add: fr o_def)
    with f show "lS. r. strict_mono  r  (f  r)  l"
      by auto
  next
    case False
    with f assms obtain l where "l  S" "U. lU  open U  infinite (U  range f)"
      by (metis image_subset_iff uncountable_def) 
    with l  S show "lS. r. strict_mono r  ((f  r)  l) sequentially"
      by (meson acc_point_range_imp_convergent_subsequence) 
  qed
qed

lemma seq_compact_eq_countably_compact:
  fixes U :: "'a :: first_countable_topology set"
  shows "seq_compact U  countably_compact U"
  by (metis countable_acc_point_imp_seq_compact countably_compact_imp_acc_point seq_compact_imp_countably_compact)

lemma seq_compact_eq_acc_point:
  fixes S :: "'a :: first_countable_topology set"
  shows "seq_compact S 
    (T. infinite T  countable T  T  S --> (xS. U. xU  open U  infinite (U  T)))"
  by (metis countable_acc_point_imp_seq_compact countably_compact_imp_acc_point seq_compact_imp_countably_compact)

lemma seq_compact_eq_compact:
  fixes U :: "'a :: second_countable_topology set"
  shows "seq_compact U  compact U"
  using seq_compact_eq_countably_compact countably_compact_eq_compact by blast

proposition Bolzano_Weierstrass_imp_seq_compact:
  fixes S :: "'a::{t1_space, first_countable_topology} set"
  shows "(T. infinite T; T  S x  S. x islimpt T)  seq_compact S"
  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)


subsectiontag unimportant› ‹Cartesian products›

lemma seq_compact_Times:
  assumes "seq_compact S" "seq_compact T"
  shows "seq_compact (S × T)"
  unfolding seq_compact_def
proof clarify
  fix h :: "nat  'a × 'b"
  assume "n. h n  S × T"
  then have *: "n. (fst  h) n  S" "n. (snd  h) n  T"
    by (simp_all add: mem_Times_iff)
  then obtain lS and rS :: "natnat"
    where "lSS" "strict_mono rS" and lS: "(fst  h  rS)  lS"
    using assms seq_compact_def by metis
  then obtain lT and rT :: "natnat" 
    where  "lTT" "strict_mono rT" and lT: "(snd  h  rS  rT)  lT"
    using assms seq_compact_def *
    by (metis (mono_tags, lifting) comp_apply) 
  have "strict_mono (rS  rT)"
    by (simp add: strict_mono rS strict_mono rT strict_mono_o)
  moreover have "(h  (rS  rT))  (lS,lT)"
    using tendsto_Pair [OF LIMSEQ_subseq_LIMSEQ [OF lS strict_mono rT] lT]
    by (simp add: o_def)
  ultimately show "lS × T. r. strict_mono r  (h  r)  l"
    using lS  S lT  T by blast
qed

lemma compact_Times:
  assumes "compact S" "compact T"
  shows "compact (S × T)"
proof (rule compactI)
  fix 𝒞
  assume C: "T𝒞. open T" "S × T  𝒞"
  have "xS. A. open A  x  A  (D𝒞. finite D  A × T  D)"
  proof
    fix x
    assume "x  S"
    have "yT. A B C. C  𝒞  open A  open B  x  A  y  B  A × B  C"
      by (smt (verit, ccfv_threshold) C UnionE x  S mem_Sigma_iff open_prod_def subsetD)
    then obtain a b c where b: "y. y  T  open (b y)"
      and c: "y. y  T  c y  𝒞  open (a y)  open (b y)  x  a y  y  b y  a y × b y  c y"
      by metis
    then have "yT. open (b y)" "T  (yT. b y)" by auto
    with compactE_image[OF compact T] obtain D where D: "D  T" "finite D" "T  (yD. b y)"
      by metis
    moreover from D c have "(yD. a y) × T  (yD. c y)"
      by (fastforce simp: subset_eq)
    ultimately show "a. open a  x  a  (d𝒞. finite d  a × T  d)"
      using c by (intro exI[of _ "c`D"] exI[of _ "(a`D)"] conjI) (auto intro!: open_INT)
  qed
  then obtain a d where a: "x. xS  open (a x)" "S  (xS. a x)"
    and d: "x. x  S  d x  𝒞  finite (d x)  a x × T  (d x)"
    unfolding subset_eq UN_iff by metis
  moreover
  from compactE_image[OF compact S a]
  obtain e where e: "e  S" "finite e" and S: "S  (xe. a x)"
    by auto
  moreover
  have "S × T  (xe. (d x))"
    by (smt (verit, del_insts) S SigmaE UN_iff d e(1) mem_Sigma_iff subset_eq)
  ultimately show "C'𝒞. finite C'  S × T  C'"
    by (intro exI[of _ "(xe. d x)"]) (auto simp: subset_eq)
qed


lemma tube_lemma:
  assumes "compact K"
  assumes "open W"
  assumes "{x0} × K  W"
  shows "X0. x0  X0  open X0  X0 × K  W"
proof -
  {
    fix y assume "y  K"
    then have "(x0, y)  W" using assms by auto
    with open W
    have "X0 Y. open X0  open Y  x0  X0  y  Y  X0 × Y  W"
      by (rule open_prod_elim) blast
  }
  then obtain X0 Y where
    *: "y  K. open (X0 y)  open (Y y)  x0  X0 y  y  Y y  X0 y × Y y  W"
    by metis
  from * have "tY ` K. open t" "K  (Y ` K)" by auto
  with compact K obtain CC where CC: "CC  Y ` K" "finite CC" "K  CC"
    by (meson compactE)
  then obtain c where c: "C. C  CC  c C  K  C = Y (c C)"
    by (force intro!: choice)
  with * CC show ?thesis
    by (force intro!: exI[where x="CCC. X0 (c C)"]) (* SLOW *)
qed

lemma continuous_on_prod_compactE:
  fixes fx::"'a::topological_space × 'b::topological_space  'c::metric_space"
    and e::real
  assumes cont_fx: "continuous_on (U × C) fx"
  assumes "compact C"
  assumes [intro]: "x0  U"
  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
  assumes "e > 0"
  obtains X0 where "x0  X0" "open X0"
    "xX0  U. t  C. dist (fx (x, t)) (fx (x0, t))  e"
proof -
  define psi where "psi = (λ(x, t). dist (fx (x, t)) (fx (x0, t)))"
  define W0 where "W0 = {(x, t)  U × C. psi (x, t) < e}"
  have W0_eq: "W0 = psi -` {..<e}  U × C"
    by (auto simp: vimage_def W0_def)
  have "open {..<e}" by simp
  have "continuous_on (U × C) psi"
    by (auto intro!: continuous_intros simp: psi_def split_beta')
  then obtain W where W: "open W" "W  U × C = W0  U × C"
    unfolding W0_eq
    by (metis open {..<e} continuous_on_open_invariant inf_right_idem) 
  have "{x0} × C  W  U × C"
    unfolding W
    by (auto simp: W0_def psi_def 0 < e)
  then have "{x0} × C  W" by blast
  from tube_lemma[OF compact C open W this]
  obtain X0 where X0: "x0  X0" "open X0" "X0 × C  W"
    by blast

  have "xX0  U. t  C. dist (fx (x, t)) (fx (x0, t))  e"
  proof safe
    fix x assume x: "x  X0" "x  U"
    fix t assume t: "t  C"
    have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
      by (auto simp: psi_def)
    also have "psi (x, t) < e"
      using W(2) W0_def X0(3) t x by fastforce
    finally show "dist (fx (x,t)) (fx (x0,t))  e" by simp
  qed
  from X0(1,2) this show ?thesis ..
qed


subsection ‹Continuity›

lemma continuous_at_imp_continuous_within:
  "continuous (at x) f  continuous (at x within s) f"
  unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto

lemma Lim_trivial_limit: "trivial_limit net  (f  l) net"
  by simp

lemmas continuous_on = continuous_on_def ― ‹legacy theorem name›

lemma continuous_within_subset:
  "continuous (at x within S) f  t  S  continuous (at x within t) f"
  unfolding continuous_within by(metis tendsto_within_subset)

lemma continuous_on_interior:
  "continuous_on S f  x  interior S  continuous (at x) f"
  by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)

lemma continuous_on_eq:
  "continuous_on S f; x. x  S  f x = g x  continuous_on S g"
  unfolding continuous_on_def tendsto_def eventually_at_topological
  by simp

text ‹Characterization of various kinds of continuity in terms of sequences.›

lemma continuous_within_sequentiallyI:
  fixes f :: "'a::{first_countable_topology, t2_space}  'b::topological_space"
  assumes "u::nat  'a. u  a  (n. u n  S)  (λn. f (u n))  f a"
  shows "continuous (at a within S) f"
  using assms unfolding continuous_within tendsto_def[where l = "f a"]
  by (auto intro!: sequentially_imp_eventually_within)

lemma continuous_within_tendsto_compose:
  fixes f::"'a::t2_space  'b::topological_space"
  assumes f: "continuous (at a within S) f"
         and  "eventually (λn. x n  S) F" "(x  a) F "
  shows "((λn. f (x n))  f a) F"
proof -
  have *: "filterlim x (inf (nhds a) (principal S)) F"
    by (simp add: assms filterlim_inf filterlim_principal)
  show ?thesis
    using "*" f continuous_within filterlim_compose tendsto_at_within_iff_tendsto_nhds by blast
qed

lemma continuous_within_tendsto_compose':
  fixes f::"'a::t2_space  'b::topological_space"
  assumes "continuous (at a within S) f"
    "n. x n  S"
    "(x  a) F "
  shows "((λn. f (x n))  f a) F"
  using always_eventually assms continuous_within_tendsto_compose by blast

lemma continuous_within_sequentially:
  fixes f :: "'a::{first_countable_topology, t2_space}  'b::topological_space"
  shows "continuous (at a within S) f 
    (x. (n::nat. x n  S)  (x  a) sequentially
          ((f  x)  f a) sequentially)"
  using continuous_within_tendsto_compose'[of a S f _ sequentially]
    continuous_within_sequentiallyI[of a S f]
  by (auto simp: o_def)

lemma continuous_at_sequentiallyI:
  fixes f :: "'a::{first_countable_topology, t2_space}  'b::topological_space"
  assumes "u. u  a  (λn. f (u n))  f a"
  shows "continuous (at a) f"
  using continuous_within_sequentiallyI[of a UNIV f] assms by auto

lemma continuous_at_sequentially:
  fixes f :: "'a::metric_space  'b::topological_space"
  shows "continuous (at a) f 
    (x. (x  a) sequentially --> ((f  x)  f a) sequentially)"
  using continuous_within_sequentially[of a UNIV f] by simp

lemma continuous_on_sequentiallyI:
  fixes f :: "'a::{first_countable_topology, t2_space}  'b::topological_space"
  assumes "u a. (n. u n  S)  a  S  u  a  (λn. f (u n))  f a"
  shows "continuous_on S f"
  using assms unfolding continuous_on_eq_continuous_within
  using continuous_within_sequentiallyI[of _ S f] by auto

lemma continuous_on_sequentially:
  fixes f :: "'a::{first_countable_topology, t2_space}  'b::topological_space"
  shows "continuous_on S f 
    (x. a  S. (n. x(n)  S)  (x  a) sequentially
       ((f  x)  f a) sequentially)"
  by (meson continuous_on_eq_continuous_within continuous_within_sequentially)

text ‹Continuity in terms of open preimages.›

lemma continuous_at_open:
  "continuous (at x) f  (t. open t  f x  t  (S. open S  x  S  (x'  S. (f x')  t)))"
  by (metis UNIV_I continuous_within_topological)

lemma continuous_imp_tendsto:
  assumes "continuous (at x0) f" and "x  x0"
  shows "(f  x)  (f x0)"
proof (rule topological_tendstoI)
  fix S
  assume "open S" "f x0  S"
  then obtain T where T_def: "open T" "x0  T" "xT. f x  S"
     using assms continuous_at_open by metis
  then have "eventually (λn. x n  T) sequentially"
    using assms T_def by (auto simp: tendsto_def)
  then show "eventually (λn. (f  x) n  S) sequentially"
    using T_def by (auto elim!: eventually_mono)
qed

subsection ‹Homeomorphisms›

definitiontag important› "homeomorphism S T f g 
  (xS. (g(f x) = x))  (f ` S = T)  continuous_on S f 
  (yT. (f(g y) = y))  (g ` T = S)  continuous_on T g"

lemma homeomorphismI [intro?]:
  assumes "continuous_on S f" "continuous_on T g"
    "f ` S  T" "g ` T  S" "x. x  S  g(f x) = x" "y. y  T  f(g y) = y"
  shows "homeomorphism S T f g"
  using assms by (force simp: homeomorphism_def)

lemma homeomorphism_translation:
  fixes a :: "'a :: real_normed_vector"
  shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)"
  unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)

lemma homeomorphism_ident: "homeomorphism T T (λa. a) (λa. a)"
  by (rule homeomorphismI) auto

lemma homeomorphism_compose:
  assumes "homeomorphism S T f g" "homeomorphism T U h k"
    shows "homeomorphism S U (h o f) (g o k)"
  using assms
  unfolding homeomorphism_def
  by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)

lemma homeomorphism_cong:
  "homeomorphism X' Y' f' g'"
    if "homeomorphism X Y f g" "X' = X" "Y' = Y" "x. x  X  f' x = f x" "y. y  Y  g' y = g y"
  using that by (auto simp add: homeomorphism_def)

lemma homeomorphism_empty [simp]:
  "homeomorphism {} {} f g"
  unfolding homeomorphism_def by auto

lemma homeomorphism_symD: "homeomorphism S t f g  homeomorphism t S g f"
  by (simp add: homeomorphism_def)

lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
  by (force simp: homeomorphism_def)

lemma continuous_on_translation_eq:
  fixes g :: "'a :: real_normed_vector  'b :: real_normed_vector"
  shows "continuous_on A ((+) a  g) = continuous_on A g"
proof -
  have g: "g = (λx. -a + x)  ((λx. a + x)  g)"
    by (rule ext) simp
  show ?thesis
    by (metis (no_types, opaque_lifting) g continuous_on_compose homeomorphism_def homeomorphism_translation)
qed

definitiontag important› homeomorphic :: "'a::topological_space set  'b::topological_space set  bool"
    (infixr "homeomorphic" 60)
  where "s homeomorphic t  (f g. homeomorphism s t f g)"

lemma homeomorphic_empty [iff]:
     "S homeomorphic {}  S = {}" "{} homeomorphic S  S = {}"
  by (auto simp: homeomorphic_def homeomorphism_def)

lemma homeomorphic_refl: "S homeomorphic S"
  using homeomorphic_def homeomorphism_ident by fastforce

lemma homeomorphic_sym: "S homeomorphic T  T homeomorphic S"
  unfolding homeomorphic_def homeomorphism_def
  by blast

lemma homeomorphic_trans [trans]:
  assumes "S homeomorphic T" and "T homeomorphic U"
  shows "S homeomorphic U"
  using assms unfolding homeomorphic_def
  by (metis homeomorphism_compose)

lemma homeomorphic_minimal:
  "S homeomorphic T 
    (f g. (xS. f(x)  T  (g(f(x)) = x)) 
           (yT. g(y)  S  (f(g(y)) = y)) 
           continuous_on S f  continuous_on T g)"
  by (smt (verit, ccfv_threshold) homeomorphic_def homeomorphismI homeomorphism_def image_eqI image_subset_iff)

lemma homeomorphicI [intro?]:
   "f ` S = T; g ` T = S;
     continuous_on S f; continuous_on T g;
     x. x  S  g(f(x)) = x;
     y. y  T  f(g(y)) = y  S homeomorphic T"
unfolding homeomorphic_def homeomorphism_def by metis

lemma homeomorphism_of_subsets:
   "homeomorphism S T f g; S'  S; T''  T; f ` S' = T'
     homeomorphism S' T' f g"
  by (smt (verit, del_insts) continuous_on_subset homeomorphismI homeomorphism_def imageE subset_eq)

lemma homeomorphism_apply1: "homeomorphism S T f g; x  S  g(f x) = x"
  by (simp add: homeomorphism_def)

lemma homeomorphism_apply2: "homeomorphism S T f g; x  T  f(g x) = x"
  by (simp add: homeomorphism_def)

lemma homeomorphism_image1: "homeomorphism S T f g  f ` S = T"
  by (simp add: homeomorphism_def)

lemma homeomorphism_image2: "homeomorphism S T f g  g ` T = S"
  by (simp add: homeomorphism_def)

lemma homeomorphism_cont1: "homeomorphism S T f g  continuous_on S f"
  by (simp add: homeomorphism_def)

lemma homeomorphism_cont2: "homeomorphism S T f g  continuous_on T g"
  by (simp add: homeomorphism_def)

lemma continuous_on_no_limpt:
   "(x. ¬ x islimpt S)  continuous_on S f"
  unfolding continuous_on_def
  by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within)

lemma continuous_on_finite:
  fixes S :: "'a::t1_space set"
  shows "finite S  continuous_on S f"
by (metis continuous_on_no_limpt islimpt_finite)

lemma homeomorphic_finite:
  fixes S :: "'a::t1_space set" and T :: "'b::t1_space set"
  assumes "finite T"
  shows "S homeomorphic T  finite S  finite T  card S = card T" (is "?lhs = ?rhs")
proof
  assume "S homeomorphic T"
  with assms show ?rhs
    by (metis (full_types) card_image_le finite_imageI homeomorphic_def homeomorphism_def le_antisym)
next
  assume R: ?rhs
  with finite_same_card_bij obtain h where "bij_betw h S T"
    by auto
  with R show ?lhs
    apply (simp only: homeomorphic_def homeomorphism_def continuous_on_finite)
    by (smt (verit, ccfv_SIG) bij_betw_imp_surj_on bij_betw_inv_into bij_betw_inv_into_left bij_betw_inv_into_right)
qed

text ‹Relatively weak hypotheses if a set is compact.›

lemma homeomorphism_compact:
  fixes f :: "'a::topological_space  'b::t2_space"
  assumes "compact S" "continuous_on S f"  "f ` S = T"  "inj_on f S"
  shows "g. homeomorphism S T f g"
proof -
  obtain g where g: "xS. g (f x) = x" "xT. f (g x) = x" "g ` T = S"
    using assms the_inv_into_f_f by fastforce 
  with assms show ?thesis
    unfolding homeomorphism_def homeomorphic_def by (metis continuous_on_inv)
qed

lemma homeomorphic_compact:
  fixes f :: "'a::topological_space  'b::t2_space"
  shows "compact S  continuous_on S f  (f ` S = T)  inj_on f S  S homeomorphic T"
  unfolding homeomorphic_def by (metis homeomorphism_compact)

text‹Preservation of topological properties.›

lemma homeomorphic_compactness: "S homeomorphic T  (compact S  compact T)"
  unfolding homeomorphic_def homeomorphism_def
  by (metis compact_continuous_image)


subsectiontag unimportant› ‹On Linorder Topologies›

lemma islimpt_greaterThanLessThan1:
  fixes a b::"'a::{linorder_topology, dense_order}"
  assumes "a < b"
  shows  "a islimpt {a<..<b}"
proof (rule islimptI)
  fix T
  assume "open T" "a  T"
  then obtain c where c: "a < c" "{a..<c}  T"
    by (meson assms open_right)
  with assms dense[of a "min c b"]
  show "y{a<..<b}. y  T  y  a"
    by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj
      not_le order.strict_implies_order subset_eq)
qed

lemma islimpt_greaterThanLessThan2:
  fixes a b::"'a::{linorder_topology, dense_order}"
  assumes "a < b"
  shows  "b islimpt {a<..<b}"
proof (rule islimptI)
  fix T
  assume "open T" "b  T"
  from open_left[OF this a < b]
  obtain c where c: "c < b" "{c<..b}  T" by auto
  with assms dense[of "max a c" b]
  show "y{a<..<b}. y  T  y  b"
    by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj
      not_le order.strict_implies_order subset_eq)
qed

lemma closure_greaterThanLessThan[simp]:
  fixes a b::"'a::{linorder_topology, dense_order}"
  shows "a < b  closure {a <..< b} = {a .. b}" (is "_  ?l = ?r")
proof
  have "?l  closure ?r"
    by (rule closure_mono) auto
  thus "closure {a<..<b}  {a..b}" by simp
qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1
  islimpt_greaterThanLessThan2)

lemma closure_greaterThan[simp]:
  fixes a b::"'a::{no_top, linorder_topology, dense_order}"
  shows "closure {a<..} = {a..}"
proof -
  from gt_ex obtain b where "a < b" by auto
  hence "{a<..} = {a<..<b}  {b..}" by auto
  also have "closure  = {a..}" using a < b unfolding closure_Un
    by auto
  finally show ?thesis .
qed

lemma closure_lessThan[simp]:
  fixes b::"'a::{no_bot, linorder_topology, dense_order}"
  shows "closure {..<b} = {..b}"
proof -
  from lt_ex obtain a where "a < b" by auto
  hence "{..<b} = {a<..<b}  {..a}" by auto
  also have "closure  = {..b}" using a < b unfolding closure_Un
    by auto
  finally show ?thesis .
qed

lemma closure_atLeastLessThan[simp]:
  fixes a b::"'a::{linorder_topology, dense_order}"
  assumes "a < b"
  shows "closure {a ..< b} = {a .. b}"
proof -
  from assms have "{a ..< b} = {a}  {a <..< b}" by auto
  also have "closure  = {a .. b}" unfolding closure_Un
    by (auto simp: assms less_imp_le)
  finally show ?thesis .
qed

lemma closure_greaterThanAtMost[simp]:
  fixes a b::"'a::{linorder_topology, dense_order}"
  assumes "a < b"
  shows "closure {a <.. b} = {a .. b}"
proof -
  from assms have "{a <.. b} = {b}  {a <..< b}" by auto
  also have "closure  = {a .. b}" unfolding closure_Un
    by (auto simp: assms less_imp_le)
  finally show ?thesis .
qed

end