--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 16 07:17:15 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 15 19:42:52 2011 -0700
@@ -20,7 +20,7 @@
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
apply(rule member_le_setL2) by auto
-subsection{* General notion of a topology *}
+subsection {* General notion of a topologies as values *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -51,7 +51,7 @@
definition "topspace T = \<Union>{S. openin T S}"
-subsection{* Main properties of open sets *}
+subsubsection {* Main properties of open sets *}
lemma openin_clauses:
fixes U :: "'a topology"
@@ -87,7 +87,7 @@
finally show "openin U S" .
qed
-subsection{* Closed sets *}
+subsubsection {* Closed sets *}
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
@@ -128,10 +128,7 @@
then show ?thesis using oS cT by (auto simp add: openin_closedin_eq)
qed
-subsection{* Subspace topology. *}
-
-term "{f x |x. P x}"
-term "{y. \<exists>x. y = f x \<and> P x}"
+subsubsection {* Subspace topology *}
definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
@@ -197,14 +194,13 @@
then show ?thesis unfolding topology_eq openin_subtopology by blast
qed
-
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
by (simp add: subtopology_superset)
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
by (simp add: subtopology_superset)
-subsection{* The universal Euclidean versions are what we use most of the time *}
+subsubsection {* The standard Euclidean topology *}
definition
euclidean :: "'a::topological_space topology" where
@@ -231,7 +227,83 @@
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
by (simp add: open_openin openin_subopen[symmetric])
-subsection{* Open and closed balls. *}
+text {* Basic "localization" results are handy for connectedness. *}
+
+lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
+ by (auto simp add: openin_subtopology open_openin[symmetric])
+
+lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
+ by (auto simp add: openin_open)
+
+lemma open_openin_trans[trans]:
+ "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
+ by (metis Int_absorb1 openin_open_Int)
+
+lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
+ by (auto simp add: openin_open)
+
+lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
+ by (simp add: closedin_subtopology closed_closedin Int_ac)
+
+lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
+ by (metis closedin_closed)
+
+lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
+ apply (subgoal_tac "S \<inter> T = T" )
+ apply auto
+ apply (frule closedin_closed_Int[of T S])
+ by simp
+
+lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
+ by (auto simp add: closedin_closed)
+
+lemma openin_euclidean_subtopology_iff:
+ fixes S U :: "'a::metric_space set"
+ shows "openin (subtopology euclidean U) S
+ \<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume ?lhs thus ?rhs unfolding openin_open open_dist by blast
+next
+ def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
+ have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
+ unfolding T_def
+ apply clarsimp
+ apply (rule_tac x="d - dist x a" in exI)
+ apply (clarsimp simp add: less_diff_eq)
+ apply (erule rev_bexI)
+ apply (rule_tac x=d in exI, clarify)
+ apply (erule le_less_trans [OF dist_triangle])
+ done
+ assume ?rhs hence 2: "S = U \<inter> T"
+ unfolding T_def
+ apply auto
+ apply (drule (1) bspec, erule rev_bexI)
+ apply auto
+ done
+ from 1 2 show ?lhs
+ unfolding openin_open open_dist by fast
+qed
+
+text {* These "transitivity" results are handy too *}
+
+lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
+ \<Longrightarrow> openin (subtopology euclidean U) S"
+ unfolding open_openin openin_open by blast
+
+lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
+ by (auto simp add: openin_open intro: openin_trans)
+
+lemma closedin_trans[trans]:
+ "closedin (subtopology euclidean T) S \<Longrightarrow>
+ closedin (subtopology euclidean U) T
+ ==> closedin (subtopology euclidean U) S"
+ by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
+
+lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
+ by (auto simp add: closedin_closed intro: closedin_trans)
+
+
+subsection {* Open and closed balls *}
definition
ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
@@ -301,82 +373,6 @@
lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
-subsection{* Basic "localization" results are handy for connectedness. *}
-
-lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
- by (auto simp add: openin_subtopology open_openin[symmetric])
-
-lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
- by (auto simp add: openin_open)
-
-lemma open_openin_trans[trans]:
- "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
- by (metis Int_absorb1 openin_open_Int)
-
-lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
- by (auto simp add: openin_open)
-
-lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
- by (simp add: closedin_subtopology closed_closedin Int_ac)
-
-lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
- by (metis closedin_closed)
-
-lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
- apply (subgoal_tac "S \<inter> T = T" )
- apply auto
- apply (frule closedin_closed_Int[of T S])
- by simp
-
-lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
- by (auto simp add: closedin_closed)
-
-lemma openin_euclidean_subtopology_iff:
- fixes S U :: "'a::metric_space set"
- shows "openin (subtopology euclidean U) S
- \<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric]
- by (simp add: open_dist) blast}
- moreover
- {assume SU: "S \<subseteq> U" and H: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x' \<in> S"
- from H obtain d where d: "\<And>x . x\<in> S \<Longrightarrow> d x > 0 \<and> (\<forall>x' \<in> U. dist x' x < d x \<longrightarrow> x' \<in> S)"
- by metis
- let ?T = "\<Union>{B. \<exists>x\<in>S. B = ball x (d x)}"
- have oT: "open ?T" by auto
- { fix x assume "x\<in>S"
- hence "x \<in> \<Union>{B. \<exists>x\<in>S. B = ball x (d x)}"
- apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto
- by (rule d [THEN conjunct1])
- hence "x\<in> ?T \<inter> U" using SU and `x\<in>S` by auto }
- moreover
- { fix y assume "y\<in>?T"
- then obtain B where "y\<in>B" "B\<in>{B. \<exists>x\<in>S. B = ball x (d x)}" by auto
- then obtain x where "x\<in>S" and x:"y \<in> ball x (d x)" by auto
- assume "y\<in>U"
- hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) }
- ultimately have "S = ?T \<inter> U" by blast
- with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast}
- ultimately show ?thesis by blast
-qed
-
-text{* These "transitivity" results are handy too. *}
-
-lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
- \<Longrightarrow> openin (subtopology euclidean U) S"
- unfolding open_openin openin_open by blast
-
-lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
- by (auto simp add: openin_open intro: openin_trans)
-
-lemma closedin_trans[trans]:
- "closedin (subtopology euclidean T) S \<Longrightarrow>
- closedin (subtopology euclidean U) T
- ==> closedin (subtopology euclidean U) S"
- by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
-
-lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
- by (auto simp add: closedin_closed intro: closedin_trans)
subsection{* Connectedness *}
@@ -430,11 +426,11 @@
lemma connected_empty[simp, intro]: "connected {}"
by (simp add: connected_def)
+
subsection{* Limit points *}
-definition
- islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool"
- (infixr "islimpt" 60) where
+definition (in topological_space)
+ islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
lemma islimptI:
@@ -469,8 +465,10 @@
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
by metis
-class perfect_space =
- assumes islimpt_UNIV [simp, intro]: "(x::'a::topological_space) islimpt UNIV"
+text {* A perfect space has no isolated points. *}
+
+class perfect_space = topological_space +
+ assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV"
lemma perfect_choose_dist:
fixes x :: "'a::{perfect_space, metric_space}"
@@ -554,7 +552,9 @@
then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
qed
-subsection{* Interior of a Set *}
+
+subsection {* Interior of a Set *}
+
definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
@@ -623,7 +623,7 @@
qed
-subsection{* Closure of a Set *}
+subsection {* Closure of a Set *}
definition "closure S = S \<union> {x | x. x islimpt S}"
@@ -793,7 +793,8 @@
unfolding closure_interior
by blast
-subsection{* Frontier (aka boundary) *}
+
+subsection {* Frontier (aka boundary) *}
definition "frontier S = closure S - interior S"
@@ -872,10 +873,9 @@
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
+
subsection {* Filters and the ``eventually true'' quantifier *}
-text {* Common filters and The "within" modifier for filters. *}
-
definition
at_infinity :: "'a::real_normed_vector filter" where
"at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
@@ -969,7 +969,6 @@
lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
unfolding trivial_limit_def ..
-
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
apply (safe elim!: trivial_limit_eventually)
apply (simp add: eventually_False [symmetric])
@@ -977,24 +976,14 @@
text{* Combining theorems for "eventually" *}
-lemma eventually_conjI:
- "\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk>
- \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net"
-by (rule eventually_conj)
-
lemma eventually_rev_mono:
"eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
using eventually_mono [of P Q] by fast
-lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
- by (auto intro!: eventually_conjI elim: eventually_rev_mono)
-
-lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
- by (auto simp add: eventually_False)
-
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
by (simp add: eventually_False)
+
subsection {* Limits *}
text{* Notation Lim to avoid collition with lim defined in analysis *}
@@ -1008,7 +997,6 @@
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
unfolding tendsto_iff trivial_limit_eq by auto
-
text{* Show that they yield usual definitions in the various cases. *}
lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
@@ -1033,7 +1021,7 @@
lemma Lim_sequentially:
"(S ---> l) sequentially \<longleftrightarrow>
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
- by (auto simp add: tendsto_iff eventually_sequentially)
+ by (rule LIMSEQ_def) (* FIXME: redundant *)
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
by (rule topological_tendstoI, auto elim: eventually_rev_mono)
@@ -1069,31 +1057,41 @@
apply (clarify, drule spec, drule (1) mp, drule (1) mp)
by (auto elim!: eventually_elim1)
+lemma eventually_within_interior:
+ assumes "x \<in> interior S"
+ shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
+proof-
+ from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
+ unfolding interior_def by fast
+ { assume "?lhs"
+ then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
+ unfolding Limits.eventually_within Limits.eventually_at_topological
+ by auto
+ with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
+ by auto
+ then have "?rhs"
+ unfolding Limits.eventually_at_topological by auto
+ } moreover
+ { assume "?rhs" hence "?lhs"
+ unfolding Limits.eventually_within
+ by (auto elim: eventually_elim1)
+ } ultimately
+ show "?thesis" ..
+qed
+
+lemma at_within_interior:
+ "x \<in> interior S \<Longrightarrow> at x within S = at x"
+ by (simp add: filter_eq_iff eventually_within_interior)
+
+lemma at_within_open:
+ "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
+ by (simp only: at_within_interior interior_open)
+
lemma Lim_within_open:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes"a \<in> S" "open S"
- shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?lhs
- { fix A assume "open A" "l \<in> A"
- with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)"
- by (rule topological_tendstoD)
- hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)"
- unfolding Limits.eventually_within .
- then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> f x \<in> A"
- unfolding eventually_at_topological by fast
- hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A"
- using assms by auto
- hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)"
- by fast
- hence "eventually (\<lambda>x. f x \<in> A) (at a)"
- unfolding eventually_at_topological .
- }
- thus ?rhs by (rule topological_tendstoI)
-next
- assume ?rhs
- thus ?lhs by (rule Lim_at_within)
-qed
+ shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
+ using assms by (simp only: at_within_open)
lemma Lim_within_LIMSEQ:
fixes a :: real and L :: "'a::metric_space"
@@ -1246,7 +1244,7 @@
hence "dist (f x) 0 < e" by (simp add: dist_norm)
}
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
- using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
+ using eventually_conj_iff[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
using assms `e>0` unfolding tendsto_iff by auto
qed
@@ -1262,7 +1260,7 @@
assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
hence "dist (f x) 0 < e" by (simp add: dist_norm)}
thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
- using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
+ using eventually_conj_iff[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
using assms `e>0` unfolding tendsto_iff by blast
qed
@@ -1295,7 +1293,7 @@
with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
by (rule tendstoD)
with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
- by (rule eventually_conjI)
+ by (rule eventually_conj)
then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
using assms(1) eventually_happens by auto
hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
@@ -1317,7 +1315,7 @@
with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
by (rule tendstoD)
with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
- by (rule eventually_conjI)
+ by (rule eventually_conj)
then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
using assms(1) eventually_happens by auto
hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
@@ -1336,7 +1334,7 @@
with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
by (rule tendstoD)
with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
- by (rule eventually_conjI)
+ by (rule eventually_conj)
then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
using assms(1) eventually_happens by auto
hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
@@ -1433,6 +1431,16 @@
using netlimit_within[of a UNIV]
by (simp add: trivial_limit_at within_UNIV)
+lemma lim_within_interior:
+ "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
+ by (simp add: at_within_interior)
+
+lemma netlimit_within_interior:
+ fixes x :: "'a::{t2_space,perfect_space}"
+ assumes "x \<in> interior S"
+ shows "netlimit (at x within S) = x"
+using assms by (simp add: at_within_interior netlimit_at)
+
text{* Transformation of limit. *}
lemma Lim_transform:
@@ -1603,7 +1611,7 @@
thus ?thesis unfolding Lim_sequentially dist_norm by simp
qed
-subsection {* More properties of closed balls. *}
+subsection {* More properties of closed balls *}
lemma closed_cball: "closed (cball x e)"
unfolding cball_def closed_def
@@ -1840,49 +1848,12 @@
shows "e = 0 ==> cball x e = {x}"
by (auto simp add: set_eq_iff)
-text{* For points in the interior, localization of limits makes no difference. *}
-
-lemma eventually_within_interior:
- assumes "x \<in> interior S"
- shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
-proof-
- from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
- unfolding interior_def by fast
- { assume "?lhs"
- then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
- unfolding Limits.eventually_within Limits.eventually_at_topological
- by auto
- with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
- by auto
- then have "?rhs"
- unfolding Limits.eventually_at_topological by auto
- } moreover
- { assume "?rhs" hence "?lhs"
- unfolding Limits.eventually_within
- by (auto elim: eventually_elim1)
- } ultimately
- show "?thesis" ..
-qed
-
-lemma at_within_interior:
- "x \<in> interior S \<Longrightarrow> at x within S = at x"
- by (simp add: filter_eq_iff eventually_within_interior)
-
-lemma lim_within_interior:
- "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
- by (simp add: at_within_interior)
-
-lemma netlimit_within_interior:
- fixes x :: "'a::{t2_space,perfect_space}"
- assumes "x \<in> interior S"
- shows "netlimit (at x within S) = x"
-using assms by (simp add: at_within_interior netlimit_at)
-
-subsection{* Boundedness. *}
+
+subsection {* Boundedness *}
(* FIXME: This has to be unified with BSEQ!! *)
-definition
- bounded :: "'a::metric_space set \<Rightarrow> bool" where
+definition (in metric_space)
+ bounded :: "'a set \<Rightarrow> bool" where
"bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
@@ -2077,7 +2048,6 @@
shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
by (rule Inf_insert, rule finite_imp_bounded, simp)
-
(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
apply (frule isGlb_isLb)
@@ -2085,6 +2055,7 @@
apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
done
+
subsection {* Equivalent versions of compactness *}
subsubsection{* Sequential compactness *}
@@ -2110,7 +2081,7 @@
Heine-Borel property if every closed and bounded subset is compact.
*}
-class heine_borel =
+class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
"bounded s \<Longrightarrow> \<forall>n. f n \<in> s
\<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
@@ -2928,7 +2899,7 @@
thus ?thesis unfolding closed_sequential_limits by fast
qed
-text{* Hence express everything as an equivalence. *}
+text {* Hence express everything as an equivalence. *}
lemma compact_eq_heine_borel:
fixes s :: "'a::metric_space set"
@@ -3117,7 +3088,8 @@
thus False using f'(3) unfolding subset_eq and Union_iff by blast
qed
-subsection{* Bounded closed nest property (proof does not use Heine-Borel). *}
+
+subsection {* Bounded closed nest property (proof does not use Heine-Borel) *}
lemma bounded_closed_nest:
assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
@@ -3147,7 +3119,7 @@
thus ?thesis by auto
qed
-text{* Decreasing case does not even need compactness, just completeness. *}
+text {* Decreasing case does not even need compactness, just completeness. *}
lemma decreasing_closed_nest:
assumes "\<forall>n. closed(s n)"
@@ -3180,7 +3152,7 @@
then show ?thesis by auto
qed
-text{* Strengthen it to the intersection actually being a singleton. *}
+text {* Strengthen it to the intersection actually being a singleton. *}
lemma decreasing_closed_nest_sing:
fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
@@ -3251,6 +3223,7 @@
ultimately show ?thesis by auto
qed
+
subsection {* Continuity *}
text {* Define continuity over a net to take in restrictions of the set. *}
@@ -3424,7 +3397,7 @@
unfolding continuous_on_def tendsto_def Limits.eventually_within
by simp
-text{* Characterization of various kinds of continuity in terms of sequences. *}
+text {* Characterization of various kinds of continuity in terms of sequences. *}
(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
lemma continuous_within_sequentially:
@@ -3799,7 +3772,7 @@
thus ?lhs unfolding continuous_on_open by auto
qed
-text{* Half-global and completely global cases. *}
+text {* Half-global and completely global cases. *}
lemma continuous_open_in_preimage:
assumes "continuous_on s f" "open t"
@@ -3867,7 +3840,7 @@
proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
-text{* Equality of continuous functions on closure and related results. *}
+text {* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -3910,7 +3883,7 @@
unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_norm)
qed
-text{* Making a continuous function avoid some value in a neighbourhood. *}
+text {* Making a continuous function avoid some value in a neighbourhood. *}
lemma continuous_within_avoid:
fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
@@ -3943,7 +3916,7 @@
shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(3,4) by auto
-text{* Proving a function is constant by proving open-ness of level set. *}
+text {* Proving a function is constant by proving open-ness of level set. *}
lemma continuous_levelset_open_in_cases:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -3966,7 +3939,7 @@
shows "\<forall>x \<in> s. f x = a"
using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
-text{* Some arithmetical combinations (more to prove). *}
+text {* Some arithmetical combinations (more to prove). *}
lemma open_scaling[intro]:
fixes s :: "'a::real_normed_vector set"
@@ -4035,7 +4008,7 @@
thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
qed
-text {* We can now extend limit compositions to consider the scalar multiplier. *}
+text {* We can now extend limit compositions to consider the scalar multiplier. *}
lemma continuous_vmul:
fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -4079,7 +4052,7 @@
uniformly_continuous_on_cmul uniformly_continuous_on_neg
uniformly_continuous_on_sub
-text{* And so we have continuity of inverse. *}
+text {* And so we have continuity of inverse. *}
lemma continuous_inv:
fixes f :: "'a::metric_space \<Rightarrow> real"
@@ -4126,7 +4099,7 @@
shows "bounded_linear f ==> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-text{* Also bilinear functions, in composition form. *}
+text {* Also bilinear functions, in composition form. *}
lemma bilinear_continuous_at_compose:
shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
@@ -4144,7 +4117,7 @@
unfolding continuous_on_def
by (fast elim: bounded_bilinear.tendsto)
-text {* Preservation of compactness and connectedness under continuous function. *}
+text {* Preservation of compactness and connectedness under continuous function. *}
lemma compact_continuous_image:
assumes "continuous_on s f" "compact s"
@@ -4176,7 +4149,7 @@
thus ?thesis unfolding connected_clopen by auto
qed
-text{* Continuity implies uniform continuity on a compact domain. *}
+text {* Continuity implies uniform continuity on a compact domain. *}
lemma compact_uniformly_continuous:
assumes "continuous_on s f" "compact s"
@@ -4238,36 +4211,40 @@
text {* A uniformly convergent limit of continuous functions is continuous. *}
-lemma norm_triangle_lt:
- fixes x y :: "'a::real_normed_vector"
- shows "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
-by (rule le_less_trans [OF norm_triangle_ineq])
-
lemma continuous_uniform_limit:
- fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
- assumes "\<not> (trivial_limit net)" "eventually (\<lambda>n. continuous_on s (f n)) net"
- "\<forall>e>0. eventually (\<lambda>n. \<forall>x \<in> s. norm(f n x - g x) < e) net"
+ fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::metric_space"
+ assumes "\<not> trivial_limit F"
+ assumes "eventually (\<lambda>n. continuous_on s (f n)) F"
+ assumes "\<forall>e>0. eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e) F"
shows "continuous_on s g"
proof-
{ fix x and e::real assume "x\<in>s" "e>0"
- have "eventually (\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3) net" using `e>0` assms(3)[THEN spec[where x="e/3"]] by auto
- then obtain n where n:"\<forall>xa\<in>s. norm (f n xa - g xa) < e / 3" "continuous_on s (f n)"
- using eventually_and[of "(\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3)" "(\<lambda>n. continuous_on s (f n))" net] assms(1,2) eventually_happens by blast
+ have "eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e / 3) F"
+ using `e>0` assms(3)[THEN spec[where x="e/3"]] by auto
+ from eventually_happens [OF eventually_conj [OF this assms(2)]]
+ obtain n where n:"\<forall>x\<in>s. dist (f n x) (g x) < e / 3" "continuous_on s (f n)"
+ using assms(1) by blast
have "e / 3 > 0" using `e>0` by auto
then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f n x') (f n x) < e / 3"
using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF `x\<in>s`, THEN spec[where x="e/3"]] by blast
- { fix y assume "y\<in>s" "dist y x < d"
- hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
- hence "norm (f n y - g x) < 2 * e / 3" using norm_triangle_lt[of "f n y - f n x" "f n x - g x" "2*e/3"]
- using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_norm unfolding ab_group_add_class.ab_diff_minus by auto
- hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
- unfolding norm_minus_cancel[of "f n y - g y", THEN sym] using norm_triangle_lt[of "f n y - g x" "g y - f n y" e] by (auto simp add: uminus_add_conv_diff) }
- hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto }
+ { fix y assume "y \<in> s" and "dist y x < d"
+ hence "dist (f n y) (f n x) < e / 3"
+ by (rule d [rule_format])
+ hence "dist (f n y) (g x) < 2 * e / 3"
+ using dist_triangle [of "f n y" "g x" "f n x"]
+ using n(1)[THEN bspec[where x=x], OF `x\<in>s`]
+ by auto
+ hence "dist (g y) (g x) < e"
+ using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
+ using dist_triangle3 [of "g y" "g x" "f n y"]
+ by auto }
+ hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
+ using `d>0` by auto }
thus ?thesis unfolding continuous_on_iff by auto
qed
-subsection{* Topological stuff lifted from and dropped to R *}
-
+
+subsection {* Topological stuff lifted from and dropped to R *}
lemma open_real:
fixes s :: "real set" shows
@@ -4312,7 +4289,7 @@
apply auto apply (rule_tac x=e in exI) apply auto
using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
-text{* Hence some handy theorems on distance, diameter etc. of/from a set. *}
+text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
lemma compact_attains_sup:
fixes s :: "real set"
@@ -4377,7 +4354,7 @@
unfolding continuous_on ..
qed
-text{* For *minimal* distance, we only need closure, not compactness. *}
+text {* For \emph{minimal} distance, we only need closure, not compactness. *}
lemma distance_attains_inf:
fixes a :: "'a::heine_borel"
@@ -4413,6 +4390,7 @@
thus ?thesis by fastsimp
qed
+
subsection {* Pasted sets *}
lemma bounded_Times:
@@ -4445,7 +4423,7 @@
apply (simp add: o_def)
done
-text{* Hence some useful properties follow quite easily. *}
+text{* Hence some useful properties follow quite easily. *}
lemma compact_scaling:
fixes s :: "'a::real_normed_vector set"
@@ -4498,7 +4476,7 @@
thus ?thesis using compact_translation[OF compact_scaling[OF assms], of a c] by auto
qed
-text{* Hence we get the following. *}
+text {* Hence we get the following. *}
lemma compact_sup_maxdistance:
fixes s :: "'a::real_normed_vector set"
@@ -4513,7 +4491,7 @@
thus ?thesis using x(2)[unfolded `x = a - b`] by blast
qed
-text{* We can state this in terms of diameter of a set. *}
+text {* We can state this in terms of diameter of a set. *}
definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
(* TODO: generalize to class metric_space *)
@@ -4566,7 +4544,7 @@
by (metis b diameter_bounded_bound order_antisym xys)
qed
-text{* Related results with closure as the conclusion. *}
+text {* Related results with closure as the conclusion. *}
lemma closed_scaling:
fixes s :: "'a::real_normed_vector set"
@@ -4694,7 +4672,8 @@
shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
unfolding frontier_def translation_diff interior_translation closure_translation by auto
-subsection{* Separation between points and sets. *}
+
+subsection {* Separation between points and sets *}
lemma separate_point_closed:
fixes s :: "'a::heine_borel set"
@@ -4737,6 +4716,7 @@
by (auto simp add: dist_commute)
qed
+
subsection {* Intervals *}
lemma interval: fixes a :: "'a::ordered_euclidean_space" shows
@@ -5169,7 +5149,69 @@
unfolding is_interval_def
by simp
-subsection{* Closure of halfspaces and hyperplanes. *}
+
+subsection {* Closure of halfspaces and hyperplanes *}
+
+lemma isCont_open_vimage:
+ assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
+proof -
+ from assms(1) have "continuous_on UNIV f"
+ unfolding isCont_def continuous_on_def within_UNIV by simp
+ hence "open {x \<in> UNIV. f x \<in> s}"
+ using open_UNIV `open s` by (rule continuous_open_preimage)
+ thus "open (f -` s)"
+ by (simp add: vimage_def)
+qed
+
+lemma isCont_closed_vimage:
+ assumes "\<And>x. isCont f x" and "closed s" shows "closed (f -` s)"
+ using assms unfolding closed_def vimage_Compl [symmetric]
+ by (rule isCont_open_vimage)
+
+lemma open_Collect_less:
+ fixes f g :: "'a::topological_space \<Rightarrow> real"
+ assumes f: "\<And>x. isCont f x"
+ assumes g: "\<And>x. isCont g x"
+ shows "open {x. f x < g x}"
+proof -
+ have "open ((\<lambda>x. g x - f x) -` {0<..})"
+ using isCont_diff [OF g f] open_real_greaterThan
+ by (rule isCont_open_vimage)
+ also have "((\<lambda>x. g x - f x) -` {0<..}) = {x. f x < g x}"
+ by auto
+ finally show ?thesis .
+qed
+
+lemma closed_Collect_le:
+ fixes f g :: "'a::topological_space \<Rightarrow> real"
+ assumes f: "\<And>x. isCont f x"
+ assumes g: "\<And>x. isCont g x"
+ shows "closed {x. f x \<le> g x}"
+proof -
+ have "closed ((\<lambda>x. g x - f x) -` {0..})"
+ using isCont_diff [OF g f] closed_real_atLeast
+ by (rule isCont_closed_vimage)
+ also have "((\<lambda>x. g x - f x) -` {0..}) = {x. f x \<le> g x}"
+ by auto
+ finally show ?thesis .
+qed
+
+lemma closed_Collect_eq:
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ assumes f: "\<And>x. isCont f x"
+ assumes g: "\<And>x. isCont g x"
+ shows "closed {x. f x = g x}"
+proof -
+ have "open {(x::'b, y::'b). x \<noteq> y}"
+ unfolding open_prod_def by (auto dest!: hausdorff)
+ hence "closed {(x::'b, y::'b). x = y}"
+ unfolding closed_def split_def Collect_neg_eq .
+ with isCont_Pair [OF f g]
+ have "closed ((\<lambda>x. (f x, g x)) -` {(x, y). x = y})"
+ by (rule isCont_closed_vimage)
+ also have "\<dots> = {x. f x = g x}" by auto
+ finally show ?thesis .
+qed
lemma Lim_inner:
assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
@@ -5187,53 +5229,37 @@
unfolding continuous_on by (rule ballI) (intro tendsto_intros)
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
-proof-
- have "\<forall>x. continuous (at x) (inner a)"
- unfolding continuous_at by (rule allI) (intro tendsto_intros)
- hence "closed (inner a -` {..b})"
- using closed_real_atMost by (rule continuous_closed_vimage)
- moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
- ultimately show ?thesis by simp
-qed
+ by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
- using closed_halfspace_le[of "-a" "-b"] unfolding inner_minus_left by auto
+ by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
lemma closed_hyperplane: "closed {x. inner a x = b}"
-proof-
- have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
- thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
-qed
+ by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
lemma closed_halfspace_component_le:
shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
- using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
+ by (intro closed_Collect_le euclidean_component.isCont isCont_const)
lemma closed_halfspace_component_ge:
shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
- using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
-
-text{* Openness of halfspaces. *}
+ by (intro closed_Collect_le euclidean_component.isCont isCont_const)
+
+text {* Openness of halfspaces. *}
lemma open_halfspace_lt: "open {x. inner a x < b}"
-proof-
- have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
- thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
-qed
+ by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
lemma open_halfspace_gt: "open {x. inner a x > b}"
-proof-
- have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
- thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
-qed
+ by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
lemma open_halfspace_component_lt:
shows "open {x::'a::euclidean_space. x$$i < a}"
- using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
+ by (intro open_Collect_less euclidean_component.isCont isCont_const)
lemma open_halfspace_component_gt:
- shows "open {x::'a::euclidean_space. x$$i > a}"
- using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
+ shows "open {x::'a::euclidean_space. x$$i > a}"
+ by (intro open_Collect_less euclidean_component.isCont isCont_const)
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
@@ -5271,28 +5297,20 @@
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {.. a}"
unfolding eucl_atMost_eq_halfspaces
-proof (safe intro!: closed_INT)
- fix i :: nat
- have "- {x::'a. x $$ i \<le> a $$ i} = {x. a $$ i < x $$ i}" by auto
- then show "closed {x::'a. x $$ i \<le> a $$ i}"
- by (simp add: closed_def open_halfspace_component_gt)
-qed
+ by (intro closed_INT ballI closed_Collect_le
+ euclidean_component.isCont isCont_const)
lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {a ..}"
unfolding eucl_atLeast_eq_halfspaces
-proof (safe intro!: closed_INT)
- fix i :: nat
- have "- {x::'a. a $$ i \<le> x $$ i} = {x. x $$ i < a $$ i}" by auto
- then show "closed {x::'a. a $$ i \<le> x $$ i}"
- by (simp add: closed_def open_halfspace_component_lt)
-qed
+ by (intro closed_INT ballI closed_Collect_le
+ euclidean_component.isCont isCont_const)
lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
by (auto intro!: continuous_open_vimage)
-text{* This gives a simple derivation of limit component bounds. *}
+text {* This gives a simple derivation of limit component bounds. *}
lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$$i \<le> b) net"
@@ -5317,7 +5335,7 @@
lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$$i = b) net"
shows "l$$i = b"
- using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
+ using ev[unfolded order_eq_iff eventually_conj_iff] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
text{* Limits relative to a union. *}
lemma eventually_within_Un:
@@ -5379,6 +5397,7 @@
using connected_ivt_hyperplane[of s x y "(basis k)::'a" a]
unfolding euclidean_component_def by auto
+
subsection {* Homeomorphisms *}
definition "homeomorphism s t f g \<equiv>
@@ -5643,7 +5662,8 @@
unfolding complete_eq_closed[THEN sym] by auto
qed
-subsection{* Some properties of a canonical subspace. *}
+
+subsection {* Some properties of a canonical subspace *}
(** move **)
declare euclidean_component.zero[simp]
@@ -5768,6 +5788,7 @@
thus ?thesis using dim_subset[OF closure_subset, of s] by auto
qed
+
subsection {* Affine transformations of intervals *}
lemma real_affinity_le:
@@ -5838,7 +5859,8 @@
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
using image_affinity_interval[of m 0 a b] by auto
-subsection{* Banach fixed point theorem (not really topological...) *}
+
+subsection {* Banach fixed point theorem (not really topological...) *}
lemma banach_fix:
assumes s:"complete s" "s \<noteq> {}" and c:"0 \<le> c" "c < 1" and f:"(f ` s) \<subseteq> s" and
@@ -5968,7 +5990,7 @@
ultimately show ?thesis using `x\<in>s` by blast+
qed
-subsection{* Edelstein fixed point theorem. *}
+subsection {* Edelstein fixed point theorem *}
lemma edelstein_fix:
fixes s :: "'a::real_normed_vector set"