Quelle Elementary_Topology.thy Sprache: Isabelle

(*  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 \<open>Topology\<close>

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

section \<open>Elementary Topology\<close>

subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>

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 (metis real_affinity_eq)

lemma image_linear_greaterThan:
  fixes x::"'a::linordered_field"
  assumes "c\0"
  shows "((\x. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})"
using  \<open>c\<noteq>0\<close>
  apply (auto simp add:image_iff field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done

lemma image_linear_lessThan:
  fixes x::"'a::linordered_field"
  assumes "c\0"
  shows "((\x. c*x+b) ` {..0 then {..
using \<open>c\<noteq>0\<close>
  apply (auto simp add:image_iff field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done

subsection \<open>Topological Basis\<close>

context topological_space
begin

definition\<^marker>\<open>tag important\<close> "topological_basis B \<longleftrightarrow>
  (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"

lemma topological_basis:
  "topological_basis B \ (\x. open x \ (\B'. B' \ B \ \B' = x))"
    (is "?lhs = ?rhs")
  by (metis bot.extremum cSup_singleton insert_subset open_Union subsetD
      topological_basis_def)

lemma topological_basis_iff:
  assumes "\B'. B' \ B \ open B'"
  shows "topological_basis B \ (\O'. open O' \ (\x\O'. \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 obtain B' where "B'\<subseteq>B" "\<Union>B' = O'"
    by (force simp add: topological_basis_def)
  then show "\B'\B. x \ B' \ B' \ O'"
    using H by auto
next
  assume H: ?rhs
  show "topological_basis B"
    unfolding topological_basis_def
  proof (intro conjI strip assms)
    fix O' :: "'a set"
    assume "open O'"
    with H obtain f where "\x\O'. f x \ B \ x \ f x \ f x \ O'"
      by metis
    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' \<in> B" "x \<in> B'" "B' \<subseteq> 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' \<subseteq> B" "S = \<Union>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 "\X\A \ 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>open S\<close>] 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 open_Times show ?thesis
    unfolding topological_basis_def
    by (smt (verit) SigmaE imageE image_mono case_prod_conv)
qed

subsection \<open>Countable Basis\<close>

locale\<^marker>\<open>tag important\<close> countable_basis = topological_space p for p::"'a set \<Rightarrow> 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' \<subseteq> B" "X = \<Union>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 \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
    "\S. open S \ x \ S \ (\A\\. A \ S)"
proof -
  obtain \<A> where \<A>: "(\<forall>i::nat. x \<in> \<A> i \<and> open (\<A> i))" "(\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> 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 \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
    "\S. open S \ x \ S \ (\A\\. A \ S)"
    "\A B. A \ \ \ B \ \ \ A \ B \ \"
proof atomize_elim
  obtain \<B> where \<B>:
    "countable \"
    "\B. B \ \ \ x \ B"
    "\B. B \ \ \ open B"
    "\S. open S \ x \ S \ \B\\. B \ S"
    by (rule first_countable_basisE) blast
  define \<A> 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) \
        (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)) \<and> (\<forall>A B. A \<in> \<A> \<longrightarrow> B \<in> \<A> \<longrightarrow> A \<inter> B \<in> \<A>)"
  proof (intro exI conjI strip)
    show "countable \"
      unfolding \<A>_def by (intro countable_image countable_Collect_finite)
    fix A
    assume "A \ \"
    then show "x \ A" "open A"
      using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> 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: \<A>_def)
    then show "A \ B \ \"
      by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
  next
    fix S
    assume "open S" "x \ S"
    then obtain a where a: "a\\" "a \ S" using \ by blast
    moreover have "a\\"
      unfolding \<A>_def
    proof (rule image_eqI)
      show "a = \ (from_nat_into \ ` {to_nat_on \ a})"
        by (simp add: \<B> 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 (intro exI[of _ "from_nat_into _"] conjI strip)
  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 \<open>\<A> \<noteq> {}\<close>] 1 by auto
next
  fix S
  assume "open S \ x\S"
  then show "\i. from_nat_into \ i \ S"
    by (metis "2" \<open>countable \<A>\<close> from_nat_into_surj)
qed

instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
proof
  fix x :: "'a \ 'b"
  obtain \<A> where \<A>:
      "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 \ \a\B. a \ S"
    by (rule first_countable_basisE[of "snd x"]) blast
  show "\\::nat \ ('a \ 'b) set.
    (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> 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: \<A>(2) B(2) mem_Times_iff x)
    show "open (a \ b)"
      by (simp add: \<A>(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) \<A>(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: \<A> 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)
    have "\B'\Inter ` {b. finite b \ b \ B}. \B' = S" if "open S" for S
    proof -
      have "\B'\{b. finite b \ b \ B}. (\b\B'. \b) = S"
        using that 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 "\k\K. \B'\{b. finite b \ b \ B}. \ (Inter ` B') = k" by auto
        then obtain k where
            "\ka\K. 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 show ?thesis
        unfolding subset_image_iff by blast
    qed
    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 \<B> :: "'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 \<F> :: "'a::second_countable_topology set set"
  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
proof -
  obtain \<B> :: "'a set set"
    where "countable \" "\C. C \ \ \ open C"
      and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
    using univ_second_countable by blast
  define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
  have "countable \"
    by (simp add: \<D>_def \<open>countable \<B>\<close>)
  have "\S. \U. S \ \ \ U \ \ \ S \ U"
    by (simp add: \<D>_def)
  then obtain G where G: "\S. S \ \ \ G S \ \ \ S \ G S"
    by metis
  have eq1: "\\ = \\"
    unfolding \<D>_def by (blast dest: \<F> \<B>)
  also have "\ = \ (G ` \)"
    using G eq1 by auto
  finally show ?thesis
    by (metis G \<open>countable \<D>\<close> countable_image image_subset_iff that)
qed

lemma countable_disjoint_open_subsets:
  fixes \<F> :: "'a::second_countable_topology set set"
  assumes "\S. S \ \ \ open S" and pw: "pairwise disjnt \"
    shows "countable \"
proof -
  obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
    by (meson assms Lindelof)
  with pw have "\ \ insert {} \'"
    by (fastforce simp add: pairwise_def disjnt_iff)
  then show ?thesis
    by (simp add: \<open>countable \<F>'\<close> 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 \<subseteq> 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.
    (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
    by (intro first_countableI[of "{b\B. 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 \<open>countable A\<close> by (simp add: Setcompr_eq_image)
  define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}"
  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
  have "\b \ B1 \ B2. x < b \ b \ y" if "x < y" for x y
  proof (cases "\z. x < z \ z < y")
    case True
    then obtain z where z: "x < z \ z < y" by auto
    define U where "U = {x<..
    then have "open U" by simp
    then obtain V where "V \ A" "z \ V" "V \ U"
      using topological_basisE[OF \<open>topological_basis A\<close>]
      by (metis U_def greaterThanLessThan_iff z)
    define w where "w = (SOME x. x \ V)"
    then have "w \ V" using \z \ V\ by (metis someI2)
    with \<open>V \<in> A\<close> \<open>V \<subseteq> U\<close> show ?thesis
      by (force simp: B2_def U_def w_def)
  next
    case False
    then have *: "\z. z > x \ z \ y" by auto
    define U where "U = {x<..}"
    then have "open U" by simp
    then obtain "V" where "V \ A" "y \ V" "V \ U"
      using topological_basisE[OF \<open>topological_basis A\<close>] U_def \<open>x < y\<close> by blast
    have "U = {y..}" unfolding U_def using * \<open>x < y\<close> 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 show ?thesis
      using B1_def \<open>V \<in> A\<close> that by blast
  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 \<open>countable A\<close> by (simp add: Setcompr_eq_image)
  define B2 where "B2 = {(SOME x. x \ U)| U. U \ A}"
  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
  have "\b \ B1 \ B2. x \ b \ b < y" if "x < y" for x y
  proof (cases "\z. x < z \ z < y")
    case True
    then obtain z where z: "x < z \ z < y" by auto
    define U where "U = {x<..
    then have "open U" by simp
    then obtain "V" where "V \ A" "z \ V" "V \ U"
      using topological_basisE[OF \<open>topological_basis A\<close>]
      by (metis U_def greaterThanLessThan_iff z)
    define w where "w = (SOME x. x \ V)"
    then have "w \ V"
      using \<open>z \<in> V\<close> by (metis someI2)
    then have "x \ w \ w < y"
      using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
    then show ?thesis
      using B2_def \<open>V \<in> A\<close> w_def by blast
  next
    case False
    then have *: "\z. z < y \ z \ x" using leI by blast
    define U where "U = {..
    then have "open U" by simp
    then obtain "V" where "V \ A" "x \ V" "V \ U"
      using topological_basisE[OF \<open>topological_basis A\<close>] U_def \<open>x < y\<close> by blast
    have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
    then have "V \ {..x}"
      using \<open>V \<subseteq> U\<close> by simp
    then have "(GREATEST x. x \ V) = x"
      using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
    then show ?thesis
      using B1_def \<open>V \<in> A\<close> that by blast
  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 \<open>x < y\<close> dense by blast
    then obtain b where "b \ B" "x < b \ b \ z" using B(2) by auto
    then show ?thesis
      using \<open>z < y\<close> by auto
  qed
  then show ?thesis using B(1) by auto
qed

subsection \<open>Polish spaces\<close>

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

class polish_space = complete_space + second_countable_topology

subsection \<open>Limit Points\<close>

definition\<^marker>\<open>tag important\<close> (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr \<open>islimpt\<close> 60)
  where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))"

lemma islimptI:
  assumes "\T. x \ T \ open T \ \y\S. 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 \<open>A perfect space has no isolated points.\<close>

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 (\x\A. B x) \ (\x\A. 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. l\U \ 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. l\U \ 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 "\y\S. y \ T \ y \ l"
    by auto
qed

lemma acc_point_range_imp_convergent_subsequence:
  fixes l :: "'a :: first_countable_topology"
  assumes l: "\U. l\U \ open U \ infinite (U \ range f)"
  shows "\r::nat\nat. 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
    have "eventually (\i. f (r i) \ A i) sequentially"
    proof
      fix i assume "Suc 0 \ i" then show "f (r i) \ A i"
        by (cases i) (simp_all add: r_def s)
    qed
    ultimately show "eventually (\i. f (r i) \ S) sequentially"
      by eventually_elim auto
  qed
  ultimately show "\r::nat\nat. 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::nat\nat. 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': "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 \<open>l' \<noteq> l\<close>] by auto
  then obtain N where "\n\N. f n \ t"
    by (meson f lim_explicit)

  have "UNIV = {.. {N..}"
    by auto
  then have "l' islimpt (f ` {.. f ` {N..})"
    by (metis l' 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 \<open>l' \<in> s\<close> \<open>open s\<close> by (rule islimptE)
  with \<open>\<forall>n\<ge>N. f n \<in> t\<close> \<open>s \<inter> t = {}\<close> 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 \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> 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] \<open>\<And>n. f n \<in> A n\<close>
    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 "\y\S. 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"
  using assms
  by (simp add: islimpt_def vimage_def continuous_on_topological Bex_def) metis


subsection \<open>Interior of a Set\<close>

definition\<^marker>\<open>tag important\<close> interior :: "('a::topological_space) set \<Rightarrow> '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"
proof
  show "interior S \ interior T \ interior (S \ T)"
    by (meson Int_mono interior_subset open_Int open_interior open_subset_interior)
qed (simp add: interior_mono)

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" "x\S"
  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 R: "open R" "x \ R" "R \ S \ T" ..
    show "x \ interior S"
    proof (rule ccontr)
      assume "x \ interior S"
      with \<open>x \<in> R\<close> \<open>open R\<close> obtain y where "y \<in> R - S"
        unfolding interior_def by fast
      with R show False
        by (metis Diff_subset_conv 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>open T\<close> unfolding open_prod_def by fast
    then have "open C" "open D" "C \ A" "D \ B" "x \ C" "y \ D"
      using \<open>T \<subseteq> A \<times> B\<close> 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>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
    with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
      by (auto simp: subset_eq Ball_def)
    with \<open>T \<subseteq> {x ..}\<close> 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>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
    with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
      by (auto simp: subset_eq Ball_def less_le)
    with \<open>T \<subseteq> {.. x}\<close> 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 \<F> :: "'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
    unfolding inj_on_def pairwise_def disjnt_def
    by (metis inf.idem int interior_Int interior_empty)
qed

subsection \<open>Closure of a Set\<close>

definition\<^marker>\<open>tag important\<close> closure :: "('a::topological_space) set \<Rightarrow> '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 T: "A \ B \ T" "closed T"
  have False
    if ab: "a \ closure A" "b \ closure B" and "(a, b) \ T" for a b
  proof -
    obtain C D where "open C" "open D" "C \ D \ - T" "a \ C" "b \ D"
      by (metis ComplI SigmaE2 \<open>closed T\<close> \<open>(a, b) \<notin> T\<close> open_Compl open_prod_elim)
    then obtain "\ C \ - A" "\ D \ - B"
      by (meson ab disjoint_iff inf_shunt open_Int_closure_eq_empty)
    then show False
      using T \<open>C \<times> D \<subseteq> - T\<close> by auto
  qed
  then show "closure A \ closure B \ T"
    by blast
qed

lemma closure_open_Int_superset:
  assumes "open S" "S \ closure T"
  shows "closure(S \ T) = closure S"
proof
  show "closure S \ closure (S \ T)"
    by (metis assms closed_closure closure_minimal inf.absorb_iff1 open_Int_closure_subset)
qed (simp add: closure_mono)

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) = (x\closure(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 \<open>Frontier (also known as boundary)\<close>

definition\<^marker>\<open>tag important\<close> frontier :: "('a::topological_space) set \<Rightarrow> '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 (simp add: Int_Un_distrib assms closed_Int frontier_closures inf_commute inf_left_commute)

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)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Filters and the ``eventually true'' quantifier\<close>

text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close>

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 (metis Diff_empty Diff_insert0 closure_subset 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 \<open>Limits\<close>

text \<open>The expected monotonicity property.\<close>

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 \<union> T = UNIV \<Longrightarrow> (f \<longlongrightarrow> l) (at x)"
  by (metis Lim_Un)

text \<open>Interrelations between restricted and unrestricted limits.\<close>

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 \<open>x < y\<close>] 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

lemma Lim_left_bound:
  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_bot} \
    'b :: {linorder_topology, conditionally_complete_linorder}"
  assumes mono: "\a b. a \ I \ b \ I \ b < x \ a \ b \ f a \ f b"
    and bnd: "\b. b \ I \ b < x \ f b \ K"
  shows "(f \ Sup (f ` ({.. I))) (at x within ({.. I))"
proof (cases "{.. I = {}")
  case True
  then show ?thesis by simp
next
  case False
  show ?thesis
  proof (rule order_tendstoI)
    fix b
    assume b: "Sup (f ` ({.. I)) < b"
    {
      fix y
      assume "y \ {.. I"
      with False bnd have "f y \ Sup (f ` ({.. I))" by (auto intro!: cSup_upper bdd_aboveI2)
      with b have "f y < b" by order
    }
    then show "eventually (\x. f x < b) (at x within ({.. I))"
      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
  next
    fix b
    assume "b < Sup (f ` ({.. I))"
    from less_cSupD[OF _ this] False obtain y where y: "y < x" "y \ I" "b < f y" by auto
    then have "eventually (\x. x \ I \ b < f x) (at_left x)"
      unfolding eventually_at_left[OF \<open>y < x\<close>] by (metis mono order_less_le order_less_le_trans)
    then show "eventually (\x. b < f x) (at x within ({.. I))"
      unfolding eventually_at_filter by eventually_elim simp
  qed
qed

text\<open>These are special for limits out of the same topological space.\<close>

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\<open>It's also sometimes useful to extract the limit point from the filter.\<close>

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\<open>Useful lemmas on closure and set of possible sequential limits.\<close>

lemma closure_sequential:
  fixes l :: "'a::first_countable_topology"
  shows "l \ closure S \ (\x. (\n. x n \ S) \ (x \ l) sequentially)"
  by (auto simp: closure_def islimpt_sequential)

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 \<longlongrightarrow> l x) (at x within S \<union> (closure S \<inter> closure T))"
  assumes g: "x \ T \ (closure S \ closure T) \
      (g \<longlongrightarrow> l x) (at x within T \<union> (closure S \<inter> 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)"
    using tendsto_within_subset[OF f] \<open>x \<in> S \<union> T\<close>
    by (metis Int_iff Un_iff Un_upper1 closure_def filterlim_at_within_closure_implies_filterlim)
  moreover
  have "(g \ l x) (at x within T - S)"
    using tendsto_within_subset g \<open>x \<in> S \<union> T\<close>
    by (metis IntI Un_Diff_Int Un_iff Un_upper1 closure_def filterlim_at_within_closure_implies_filterlim)
  ultimately show ?thesis
    by (intro filterlim_at_within_If) (simp_all only: *)
qed

subsection \<open>Compactness\<close>

lemma brouwer_compactness_lemma:
  fixes f :: "'a::topological_space \ 'b::real_normed_vector"
  assumes "compact S"
    and "continuous_on S f"
    and "\ (\x\S. f x = 0)"
  obtains d where "0 < d" and "\x\S. 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" "\y\S. (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 \<open>Bolzano-Weierstrass property\<close>

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: "\x\S. x \ f x \ open (f x) \ (\y\T. 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. x\S \ T = f x}"]]
    using f by auto
  then have g': "\x\g. \y \ S. x = f y"
    by auto
  have "inj_on f T"
    unfolding inj_on_def using \<open>T \<subseteq> S\<close> f by blast
  then have "infinite (f ` T)"
    using assms(2) using finite_imageD by auto
  moreover
  have False if "x \ T" "f x \ g" for x
    using \<open>T \<subseteq> S\<close>  f g' \<open>S \<subseteq> \<Union>g\<close> that by force
  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 \<open>finite (range f)\<close> 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 \<section>: "\<forall>n. x n \<in> S" "(x \<longlongrightarrow> l) sequentially"
    have "l \ S"
    proof (cases "\n. x n \ l")
      case True
      with \<section> have "infinite (range x)"
        using sequence_infinite_lemma[of x l] by auto
      with \<section> assms show "l\<in>S"
        using sequence_unique_limpt \<section> True by blast
    qed (use \<section> in auto)
  }
  then show ?thesis
    unfolding closed_sequential_limits by auto
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\<open>In particular, some common special cases.\<close>

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 * \<open>compact S\<close> obtain s' where "s' \<subseteq> f \<and> finite s' \<and> S \<subseteq> \<Union>s'"
    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
  moreover
  from * \<open>compact T\<close> obtain t' where "t' \<subseteq> f \<and> finite t' \<and> T \<subseteq> \<Union>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 (\x\A. 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)

--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.