(* 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 (simp add: field_simps)
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))"
unfolding topological_basis_def
apply safe
apply fastforce
apply fastforce
apply (erule_tac x=x in allE, simp)
apply (rule_tac x="{x}" in exI, auto)
done
lemma topological_basis_iff:
assumes "\B'. B' \ B \ open B'"
shows "topological_basis B \ (\O'. open O' \ (\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 have "(\B'\B. \B' = O')" by (simp add: topological_basis_def)
then obtain B' where "B' \<subseteq> B" "O' = \<Union>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 "\x\O'. f x \ B \ x \ f x \ f x \ O'"
by (force intro: bchoice simp: Bex_def)
then show "\B'\B. \B' = O'"
by (auto intro: exI[where x="{f x |x. x \ O'}"])
qed
qed
lemma topological_basisI:
assumes "\B'. B' \ B \ open B'"
and "\O' x. open O' \ x \ O' \ \B'\B. x \ B' \ B' \ O'"
shows "topological_basis B"
using assms by (subst topological_basis_iff) auto
lemma topological_basisE:
fixes O'
assumes "topological_basis B"
and "open O'"
and "x \ O'"
obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
proof atomize_elim
from assms have "\B'. B'\B \ open B'"
by (simp add: topological_basis_def)
with topological_basis_iff assms
show "\B'. B' \ B \ x \ B' \ B' \ O'"
using assms by (simp add: Bex_def)
qed
lemma topological_basis_open:
assumes "topological_basis B"
and "X \ B"
shows "open X"
using assms by (simp add: topological_basis_def)
lemma topological_basis_imp_subbasis:
assumes B: "topological_basis B"
shows "open = generate_topology B"
proof (intro ext iffI)
fix S :: "'a set"
assume "open S"
with B obtain B' where "B' \<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 choosefrom_basis: "\B'. B' \ {} \ f B' \ B'"
shows "\X. open X \ X \ {} \ (\B' \ B. f B' \ X)"
proof (intro allI impI)
fix X :: "'a set"
assume "open X" and "X \ {}"
from topological_basisE[OF \<open>topological_basis B\<close> \<open>open X\<close> choosefrom_basis[OF \<open>X \<noteq> {}\<close>]]
obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
then show "\B'\B. f B' \ X"
by (auto intro!: choosefrom_basis)
qed
end
lemma topological_basis_prod:
assumes A: "topological_basis A"
and B: "topological_basis B"
shows "topological_basis ((\(a, b). a \ b) ` (A \ B))"
unfolding topological_basis_def
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
fix S :: "('a \ 'b) set"
assume "open S"
then show "\X\A \ B. (\(a,b)\X. a \ b) = S"
proof (safe intro!: exI[of _ "{x\A \ B. fst x \ snd x \ S}"])
fix x y
assume "(x, y) \ S"
from open_prod_elim[OF \<open>open S\<close> this]
obtain a b where a: "open a""x \ a" and b: "open b" "y \ b" and "a \ b \ S"
by (metis mem_Sigma_iff)
moreover
from A a obtain A0 where "A0 \ A" "x \ A0" "A0 \ a"
by (rule topological_basisE)
moreover
from B b obtain B0 where "B0 \ B" "y \ B0" "B0 \ b"
by (rule topological_basisE)
ultimately show "(x, y) \ (\(a, b)\{X \ A \ B. fst X \ snd X \ S}. a \ b)"
by (intro UN_I[of "(A0, B0)"]) auto
qed auto
qed (metis A B topological_basis_open open_Times)
subsection \<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 atomize_elim simp
lemma countable_dense_exists:
"\D::'a set. countable D \ (\X. p X \ X \ {} \ (\d \ D. d \ X))"
proof -
let ?f = "(\B'. SOME x. x \ B')"
have "countable (?f ` B)" using countable_basis by simp
with basis_dense[OF is_basis, of ?f] show ?thesis
by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
qed
lemma countable_dense_setE:
obtains D :: "'a set"
where "countable D" "\X. p X \ X \ {} \ \d \ D. d \ X"
using countable_dense_exists by blast
end
lemma countable_basis_openI: "countable_basis open B"
if "countable B" "topological_basis B"
using that
by unfold_locales
(simp_all add: topological_basis topological_space.topological_basis topological_space_axioms)
lemma (in first_countable_topology) first_countable_basisE:
fixes x :: 'a
obtains \<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
show thesis
proof
show "countable (range \)"
by simp
qed (use \<A> in auto)
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 (safe intro!: exI[where x=\<A>])
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
then show "\a\\. a \ S" using a \
by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"])
qed
qed
lemma (in topological_space) first_countableI:
assumes "countable \"
and 1: "\A. A \ \ \ x \ A" "\A. A \ \ \ open A"
and 2: "\S. open S \ x \ S \ \A\\. A \ S"
shows "\\::nat \ 'a set. (\i. x \ \ i \ open (\ i)) \ (\S. open S \ x \ S \ (\i. \ i \ S))"
proof (safe intro!: exI[of _ "from_nat_into \"])
fix i
have "\ \ {}" using 2[of UNIV] by auto
show "x \ from_nat_into \ i" "open (from_nat_into \ i)"
using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
next
fix S
assume "open S" "x\S" from 2[OF this]
show "\i. from_nat_into \ i \ S"
using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto
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
from a'b' \<A>(4)[of a'] B(4)[of b']
obtain a b where "a \ \" "a \ a'" "b \ B" "b \ b'"
by auto
ultimately
show "\a\(\(a, b). a \ b) ` (\ \ B). a \ S"
by (auto intro!: bexI[of _ "a \ b"] bexI[of _ a] bexI[of _ b])
qed (simp add: \<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)
{
fix S
assume "open S"
then have "\B'\{b. finite b \ b \ B}. (\b\B'. \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 "\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 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 \<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 \"
apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
apply (force simp: \<D>_def)
done
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 "\\ \ \\"
unfolding \<D>_def by (blast dest: \<F> \<B>)
moreover have "\\ \ \\"
using \<D>_def by blast
ultimately have eq1: "\\ = \\" ..
have eq2: "\\ = \ (G ` \)"
using G eq1 by auto
show ?thesis
apply (rule_tac \<F>' = "G ` \<D>" in that)
using G \<open>countable \<D>\<close>
by (auto simp: eq1 eq2)
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)
assume "\z. x < z \ z < y"
then obtain z where z: "x < z \ z < y" by auto
define U where "U = {x<..
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 \<open>topological_basis A\<close>] 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 \<open>topological_basis A\<close>] by auto
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 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 \<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)
assume "\z. x < z \ z < y"
then obtain z where z: "x < z \ z < y" by auto
define U where "U = {x<..
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 \<open>topological_basis A\<close>] 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 = {..
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 \<open>topological_basis A\<close>] by auto
have "U = {..x}" unfolding U_def using * \<open>x < y\<close> 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 \<open>x < y\<close> 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 \<open>b \<in> B\<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 "islimpt" 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
apply (subst open_subopen)
apply (simp add: islimpt_def subset_eq)
apply (metis ComplE ComplI)
done
lemma islimpt_EMPTY[simp]: "\ x islimpt {}"
by (auto simp: islimpt_def)
lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T"
by (simp add: islimpt_iff_eventually eventually_conj_iff)
lemma islimpt_insert:
fixes x :: "'a::t1_space"
shows "x islimpt (insert a s) \ x islimpt s"
proof
assume *: "x islimpt (insert a s)"
show "x islimpt s"
proof (rule islimptI)
fix t
assume t: "x \ t" "open t"
show "\y\s. y \ t \ y \ x"
proof (cases "x = a")
case True
obtain y where "y \ insert a s" "y \ t" "y \ x"
using * t by (rule islimptE)
with \<open>x = a\<close> show ?thesis by auto
next
case False
with t have t': "x \ t - {a}" "open (t - {a})"
by (simp_all add: open_Diff)
obtain y where "y \ insert a s" "y \ t - {a}" "y \ x"
using * t' by (rule islimptE)
then show ?thesis by auto
qed
qed
next
assume "x islimpt s"
then show "x islimpt (insert a s)"
by (rule islimpt_subset) auto
qed
lemma islimpt_finite:
fixes x :: "'a::t1_space"
shows "finite s \ \ x islimpt s"
by (induct set: finite) (simp_all add: islimpt_insert)
lemma islimpt_Un_finite:
fixes x :: "'a::t1_space"
shows "finite s \ x islimpt (s \ t) \ x islimpt t"
by (simp add: islimpt_Un islimpt_finite)
lemma islimpt_eq_acc_point:
fixes l :: "'a :: t1_space"
shows "l islimpt S \ (\U. 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 "infinite (T \ S - {l})"
by auto
then have "\x. x \ (T \ S - {l})"
unfolding ex_in_conv by (intro notI) simp
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}"
unfolding ex_in_conv by (intro notI) simp
then have "\j. f j \ A (Suc n) \ j \ {.. i}"
by auto
then have "\a. i < a \ f a \ A (Suc n)"
by (auto simp: not_le)
then have "i < s n i" "f (s n i) \ A (Suc n)"
unfolding s_def by (auto intro: someI2_ex)
}
note s = this
define r where "r = rec_nat (s 0 0) s"
have "strict_mono r"
by (auto simp: r_def s strict_mono_Suc_iff)
moreover
have "(\n. f (r n)) \ l"
proof (rule topological_tendstoI)
fix S
assume "open S" "l \ S"
with A(3) have "eventually (\i. A i \ S) sequentially"
by auto
moreover
{
fix i
assume "Suc 0 \ i"
then have "f (r i) \ A i"
by (cases i) (simp_all add: r_def s)
}
then have "eventually (\i. f (r i) \ A i) sequentially"
by (auto simp: eventually_sequentially)
ultimately show "eventually (\i. f (r i) \ S) sequentially"
by eventually_elim auto
qed
ultimately show "\r::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 \ 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 \<open>l' \<noteq> l\<close>] by auto
have "eventually (\n. f n \ t) sequentially"
using assms(1) \<open>open t\<close> \<open>l \<in> t\<close> by (rule topological_tendstoD)
then obtain N where "\n\N. f n \ t"
unfolding eventually_sequentially by auto
have "UNIV = {.. {N..}"
by auto
then have "l' islimpt (f ` ({.. {N..}))"
using assms(2) by simp
then have "l' islimpt (f ` {.. 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 \<open>l' \<in> s\<close> \<open>open s\<close> by (rule islimptE)
then obtain n where "N \ n" "f n \ s" "f n \ l'"
by auto
with \<open>\<forall>n\<ge>N. f n \<in> t\<close> have "f n \<in> s \<inter> t"
by simp
with \<open>s \<inter> t = {}\<close> show False
by simp
qed
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"
by (meson Int_mono Int_subset_iff antisym_conv interior_maximal interior_subset open_Int open_interior)
lemma eventually_nhds_in_nhd: "x \ interior s \ eventually (\y. y \ s) (nhds x)"
using interior_subset[of s] by (subst eventually_nhds) blast
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
assumes x: "x \ interior S"
shows "x islimpt S"
using x islimpt_UNIV [of x]
unfolding interior_def islimpt_def
apply (clarsimp, rename_tac T T')
apply (drule_tac x="T \ T'" in spec)
apply (auto simp: open_Int)
done
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S"
and iT: "interior T = {}"
shows "interior (S \ T) = interior S"
proof
show "interior S \ interior (S \ T)"
by (rule interior_mono) (rule Un_upper1)
show "interior (S \ T) \ interior S"
proof
fix x
assume "x \ interior (S \ T)"
then obtain R where "open R" "x \ R" "R \ S \ T" ..
show "x \ interior S"
proof (rule ccontr)
assume "x \ interior S"
with \<open>x \<in> R\<close> \<open>open R\<close> obtain y where "y \<in> R - S"
unfolding interior_def by fast
from \<open>open R\<close> \<open>closed S\<close> have "open (R - S)"
by (rule open_Diff)
from \<open>R \<subseteq> S \<union> T\<close> have "R - S \<subseteq> T"
by fast
from \<open>y \<in> R - S\<close> \<open>open (R - S)\<close> \<open>R - S \<subseteq> T\<close> \<open>interior T = {}\<close> show False
unfolding interior_def by fast
qed
qed
qed
lemma interior_Times: "interior (A \ B) = interior A \ interior B"
proof (rule interior_unique)
show "interior A \ interior B \ A \ B"
by (intro Sigma_mono interior_subset)
show "open (interior A \ interior B)"
by (intro open_Times open_interior)
fix T
assume "T \ A \ B" and "open T"
then show "T \ interior A \ interior B"
proof safe
fix x y
assume "(x, y) \ T"
then obtain C D where "open C" "open D" "C \ D \ T" "x \ C" "y \ D"
using \<open>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 apply (clarsimp simp: inj_on_def pairwise_def)
apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
done
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"
have "x islimpt (S \ T)" if **: "x islimpt T"
proof (rule islimptI)
fix A
assume "x \ A" "open A"
with * have "x \ A \ S" "open (A \ S)"
by (simp_all add: open_Int)
with ** obtain y where "y \ T" "y \ A \ S" "y \ x"
by (rule islimptE)
then have "y \ S \ T" "y \ A \ y \ x"
by simp_all
then show "\y\(S \ T). y \ A \ y \ x" ..
qed
with * show "x \ closure (S \ T)"
unfolding closure_def by blast
qed
lemma closure_complement: "closure (- S) = - interior S"
by (simp add: closure_interior)
lemma interior_complement: "interior (- S) = - closure S"
by (simp add: closure_interior)
lemma interior_diff: "interior(S - T) = interior S - closure T"
by (simp add: Diff_eq interior_complement)
lemma closure_Times: "closure (A \ B) = closure A \ closure B"
proof (rule closure_unique)
show "A \ B \ closure A \ closure B"
by (intro Sigma_mono closure_subset)
show "closed (closure A \ closure B)"
by (intro closed_Times closed_closure)
fix T
assume "A \ B \ T" and "closed T"
then show "closure A \ closure B \ T"
apply (simp add: closed_def open_prod_def, clarify)
apply (rule ccontr)
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
apply (simp add: closure_interior interior_def)
apply (drule_tac x=C in spec)
apply (drule_tac x=D in spec, auto)
done
qed
lemma closure_open_Int_superset:
assumes "open S" "S \ closure T"
shows "closure(S \ T) = closure S"
proof -
have "closure S \ closure(S \ T)"
by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
then show ?thesis
by (simp add: closure_mono dual_order.antisym)
qed
lemma closure_Int: "closure (\I) \ \{closure S |S. S \ I}"
proof -
{
fix y
assume "y \ \I"
then have y: "\S \ I. y \ S" by auto
{
fix S
assume "S \ I"
then have "y \ closure S"
using closure_subset y by auto
}
then have "y \ \{closure S |S. S \ I}"
by auto
}
then have "\I \ \{closure S |S. S \ I}"
by auto
moreover have "closed (\{closure S |S. S \ I})"
unfolding closed_Inter closed_closure by auto
ultimately show ?thesis using closure_hull[of "\I"]
hull_minimal[of "\I" "\{closure S |S. S \ I}" "closed"] by auto
qed
lemma islimpt_in_closure: "(x islimpt S) = (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)"
proof -
have "closure (S \ T) = T \ S"
using assms by (simp add: Int_commute closed_Int)
moreover have "T \ (closure S \ closure (- S)) = frontier S \ T"
by (simp add: Int_commute frontier_closures)
ultimately show ?thesis
by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
qed
lemma frontier_subset_closed: "closed S \ frontier S \ S"
by (metis frontier_def closure_closed Diff_subset)
lemma frontier_empty [simp]: "frontier {} = {}"
by (simp add: frontier_def)
lemma frontier_subset_eq: "frontier S \ S \ closed S"
proof -
{
assume "frontier S \ S"
then have "closure S \ S"
using interior_subset unfolding frontier_def by auto
then have "closed S"
using closure_subset_eq by auto
}
then show ?thesis using frontier_subset_closed[of S] ..
qed
lemma frontier_complement [simp]: "frontier (- S) = frontier S"
by (auto simp: frontier_def closure_complement interior_complement)
lemma frontier_Un_subset: "frontier(S \ T) \ frontier S \ frontier T"
by (metis compl_sup frontier_Int_subset frontier_complement)
lemma frontier_disjoint_eq: "frontier S \ S = {} \ open S"
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
lemma frontier_UNIV [simp]: "frontier UNIV = {}"
using frontier_complement frontier_empty by fastforce
lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
by (simp add: Int_commute frontier_def interior_closure)
lemma frontier_interior_subset: "frontier(interior S) \ frontier S"
by (simp add: Diff_mono frontier_interiors interior_mono interior_subset)
lemma closure_Un_frontier: "closure S = S \ frontier S"
proof -
have "S \ interior S = S"
using interior_subset by auto
then show ?thesis
using closure_subset by (auto simp: frontier_def)
qed
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"
proof
assume "trivial_limit (at a within S)"
then show "\ a islimpt S"
unfolding trivial_limit_def
unfolding eventually_at_topological
unfolding islimpt_def
apply (clarsimp simp add: set_eq_iff)
apply (rename_tac T, rule_tac x=T in exI)
apply (clarsimp, drule_tac x=y in bspec, simp_all)
done
next
assume "\ a islimpt S"
then show "trivial_limit (at a within S)"
unfolding trivial_limit_def eventually_at_topological islimpt_def
by metis
qed
lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV"
using trivial_limit_within [of a UNIV] by simp
lemma trivial_limit_at: "\ trivial_limit (at a)"
for a :: "'a::perfect_space"
by (rule at_neq_bot)
lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))"
using islimpt_in_closure by (metis trivial_limit_within)
lemma not_in_closure_trivial_limitI:
"x \ closure s \ trivial_limit (at x within s)"
using not_trivial_limit_within[of x s]
by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
if "x \ closure s \ filterlim f l (at x within s)"
by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
lemma at_within_eq_bot_iff: "at c within A = bot \ c \ closure (A - {c})"
using not_trivial_limit_within[of c A] by blast
text \<open>Some property holds "sufficiently close" to the limit point.\<close>
lemma trivial_limit_eventually: "trivial_limit net \ eventually P net"
by simp
lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)"
by (simp add: filter_eq_iff)
lemma Lim_topological:
"(f \ l) net \
trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
unfolding tendsto_def trivial_limit_eq by auto
lemma eventually_within_Un:
"eventually P (at x within (s \ t)) \
eventually P (at x within s) \<and> eventually P (at x within t)"
unfolding eventually_at_filter
by (auto elim!: eventually_rev_mp)
lemma Lim_within_union:
"(f \ l) (at x within (s \ t)) \
(f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
unfolding tendsto_def
by (auto simp: eventually_within_Un)
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)"
(is "?lhs = ?rhs")
proof
from assms obtain T where T: "open T" "x \ T" "T \ S" ..
{
assume ?lhs
then obtain A where "open A" and "x \ A" and "\y\A. y \ x \ y \ S \ P y"
by (auto simp: eventually_at_topological)
with T have "open (A \ T)" and "x \ A \ T" and "\y \ A \ T. y \ x \ P y"
by auto
then show ?rhs
by (auto simp: eventually_at_topological)
next
assume ?rhs
then show ?lhs
by (auto elim: eventually_mono simp: eventually_at_filter)
}
qed
lemma at_within_interior: "x \ interior S \ at x within S = at x"
unfolding filter_eq_iff by (intro allI eventually_within_interior)
lemma Lim_within_LIMSEQ:
fixes a :: "'a::first_countable_topology"
assumes "\S. (\n. S n \ a \ S n \ T) \ S \ a \ (\n. X (S n)) \ L"
shows "(X \ L) (at a within T)"
using assms unfolding tendsto_def [where l=L]
by (simp add: sequentially_imp_eventually_within)
lemma Lim_right_bound:
fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \
'b::{linorder_topology, conditionally_complete_linorder}"
assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b"
and bnd: "\a. a \ I \ x < a \ K \ f a"
shows "(f \ Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))"
proof (cases "{x<..} \ I = {}")
case True
then show ?thesis by simp
next
case False
show ?thesis
proof (rule order_tendstoI)
fix a
assume a: "a < Inf (f ` ({x<..} \ I))"
{
fix y
assume "y \ {x<..} \ I"
with False bnd have "Inf (f ` ({x<..} \ I)) \ f y"
by (auto intro!: cInf_lower bdd_belowI2)
with a have "a < f y"
by (blast intro: less_le_trans)
}
then show "eventually (\x. a < f x) (at x within ({x<..} \ I))"
by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
next
fix a
assume "Inf (f ` ({x<..} \ I)) < a"
from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \ I" "f y < a"
by auto
then have "eventually (\x. x \ I \ f x < a) (at_right x)"
unfolding eventually_at_right[OF \<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
(*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
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)"
(is "?lhs = ?rhs")
proof
assume "?lhs"
moreover
{
assume "l \ S"
then have "?rhs" using tendsto_const[of l sequentially] by auto
}
moreover
{
assume "l islimpt S"
then have "?rhs" unfolding islimpt_sequential by auto
}
ultimately show "?rhs"
unfolding closure_def by auto
next
assume "?rhs"
then show "?lhs" unfolding closure_def islimpt_sequential by auto
qed
lemma closed_sequential_limits:
fixes S :: "'a::first_countable_topology set"
shows "closed S \ (\x l. (\n. x n \ S) \ (x \ l) sequentially \ l \ S)"
by (metis closure_sequential closure_subset_eq subset_iff)
lemma tendsto_If_within_closures:
assumes f: "x \ s \ (closure s \ closure t) \
(f \<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)"
by (rule filterlim_at_within_closure_implies_filterlim)
(use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
moreover
have "(g \ l x) (at x within t - s)"
by (rule filterlim_at_within_closure_implies_filterlim)
(use \<open>x \<in> _\<close> in
\<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
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
have "(norm \ f) x > 0"
using assms(3) and x(1)
by auto
then show ?thesis
by (rule that) (insert x(2), auto simp: o_def)
qed
subsubsection \<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
using bchoice[of s "\ x T. x \ T \ open T \ (\y\t. y \ T \ y = x)"]
by auto
obtain g where g: "g \ {t. \x. x \ s \ t = f x}" "finite g" "s \ \g"
using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]]
using f by auto
from g(1,3) have g':"\x\g. \xa \ s. x = f xa"
by auto
{
fix x y
assume "x \ t" "y \ t" "f x = f y"
then have "x \ f x" "y \ f x \ y = x"
using f[THEN bspec[where x=x]] and \<open>t \<subseteq> s\<close> by auto
then have "x = y"
using \<open>f x = f y\<close> and f[THEN bspec[where x=y]] and \<open>y \<in> t\<close> and \<open>t \<subseteq> s\<close>
by auto
}
then have "inj_on f t"
unfolding inj_on_def by simp
then have "infinite (f ` t)"
using assms(2) using finite_imageD by auto
moreover
{
fix x
assume "x \ t" "f x \ g"
from g(3) assms(3) \<open>x \<in> t\<close> obtain h where "h \<in> g" and "x \<in> h"
by auto
then obtain y where "y \ s" "h = f y"
using g'[THEN bspec[where x=h]] by auto
then have "y = x"
using f[THEN bspec[where x=y]] and \<open>x\<in>t\<close> and \<open>x\<in>h\<close>[unfolded \<open>h = f y\<close>]
by auto
then have False
using \<open>f x \<notin> g\<close> \<open>h \<in> g\<close> unfolding \<open>h = f y\<close>
by auto
}
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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.54 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
