--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue May 08 21:03:06 2018 +0100
@@ -1978,7 +1978,7 @@
and measure_countable_negligible_Union_bounded: "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
proof -
obtain a b where ab: "(\<Union>n. S n) \<subseteq> cbox a b"
- using bo bounded_subset_cbox by blast
+ using bo bounded_subset_cbox_symmetric by metis
then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
proof -
have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
@@ -2837,7 +2837,7 @@
if "bounded S" "S \<in> lmeasurable" for S
proof -
obtain a b where "S \<subseteq> cbox a b"
- using \<open>bounded S\<close> bounded_subset_cbox by blast
+ using \<open>bounded S\<close> bounded_subset_cbox_symmetric by metis
have fUD: "(f ` \<Union>\<D>) \<in> lmeasurable \<and> ?\<mu> (f ` \<Union>\<D>) = (m * ?\<mu> (\<Union>\<D>))"
if "countable \<D>"
and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<subseteq> cbox a b \<and> K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
@@ -3005,7 +3005,7 @@
"\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> \<bar>?\<mu> (S \<inter> cbox a b) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)"
using has_measure_limit [OF S] \<open>e > 0\<close> by (metis abs_add_one_gt_zero zero_less_divide_iff)
obtain c d::'n where cd: "ball 0 B \<subseteq> cbox c d"
- using bounded_subset_cbox by blast
+ by (metis bounded_subset_cbox_symmetric bounded_ball)
with B have less: "\<bar>?\<mu> (S \<inter> cbox c d) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)" .
obtain D where "D > 0" and D: "cbox c d \<subseteq> ball 0 D"
by (metis bounded_cbox bounded_subset_ballD)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue May 08 21:03:06 2018 +0100
@@ -334,7 +334,7 @@
\<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
- by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
+ by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox_symmetric)
obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
using B1(2)[OF ab(1)] by blast
obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
@@ -1635,9 +1635,9 @@
using has_integral_altD[OF _ False ij] assms by blast
have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
unfolding bounded_Un by(rule conjI bounded_ball)+
- from bounded_subset_cbox[OF this]
+ from bounded_subset_cbox_symmetric[OF this]
obtain a b::'a where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
- by blast+
+ by (meson Un_subset_iff)
then obtain w1 w2 where int_w1: "((\<lambda>x. if x \<in> S then f x else 0) has_integral w1) (cbox a b)"
and norm_w1: "norm (w1 - i) < (i \<bullet> k - j \<bullet> k) / 3"
and int_w2: "((\<lambda>x. if x \<in> S then g x else 0) has_integral w2) (cbox a b)"
@@ -6227,7 +6227,7 @@
\<exists>z. (?g has_integral z) (cbox a b) \<and> norm (z - integral S g) < e/2"
using integrable_integral [OF int_g,unfolded has_integral'[of g]] e that by blast
obtain a b::'n where ab: "ball 0 Bf \<union> ball 0 Bg \<subseteq> cbox a b"
- using ball_max_Un bounded_subset_cbox[OF bounded_ball, of _ "max Bf Bg"] by blast
+ using ball_max_Un by (metis bounded_ball bounded_subset_cbox_symmetric)
have "ball 0 Bf \<subseteq> cbox a b"
using ab by auto
with Bf obtain z where int_fz: "(?f has_integral z) (cbox a b)" and z: "norm (z - integral S f) < e/2"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue May 08 21:03:06 2018 +0100
@@ -908,14 +908,17 @@
qed (simp add: borel_prod[symmetric])
(* FIXME: conversion in measurable prover *)
-lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
-lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
+lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel"
+ by simp
+
+lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel"
+ by simp
lemma emeasure_bounded_finite:
assumes "bounded A" shows "emeasure lborel A < \<infinity>"
proof -
- from bounded_subset_cbox[OF \<open>bounded A\<close>] obtain a b where "A \<subseteq> cbox a b"
- by auto
+ obtain a b where "A \<subseteq> cbox a b"
+ by (meson bounded_subset_cbox_symmetric \<open>bounded A\<close>)
then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
by (intro emeasure_mono) auto
then show ?thesis
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue May 08 21:03:06 2018 +0100
@@ -267,7 +267,7 @@
and bdd_below_box[intro, simp]: "bdd_below (box a b)"
unfolding atomize_conj
by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
- bounded_subset_cbox interval_cbox)
+ bounded_subset_cbox_symmetric interval_cbox)
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
begin
--- a/src/HOL/Analysis/Path_Connected.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Tue May 08 21:03:06 2018 +0100
@@ -6981,7 +6981,7 @@
shows "S = {}"
proof -
obtain a b where "S \<subseteq> box a b"
- by (meson assms bounded_subset_open_interval)
+ by (meson assms bounded_subset_box_symmetric)
then have "a \<notin> S" "b \<notin> S"
by auto
then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"
--- a/src/HOL/Analysis/Tagged_Division.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Tue May 08 21:03:06 2018 +0100
@@ -685,7 +685,7 @@
lemma elementary_subset_cbox:
"p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
- by (meson elementary_bounded bounded_subset_cbox)
+ by (meson bounded_subset_cbox_symmetric elementary_bounded)
lemma division_union_intervals_exists:
fixes a b :: "'a::euclidean_space"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue May 08 21:03:06 2018 +0100
@@ -47,19 +47,19 @@
lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}"
by (auto simp: support_on_def)
-lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)"
+lemma finite_support[intro]: "finite S \<Longrightarrow> finite (support_on S f)"
unfolding support_on_def by auto
(* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *)
definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
- where "supp_sum f s = (\<Sum>x\<in>support_on s f. f x)"
+ where "supp_sum f S = (\<Sum>x\<in>support_on S f. f x)"
lemma supp_sum_empty[simp]: "supp_sum f {} = 0"
unfolding supp_sum_def by auto
lemma supp_sum_insert[simp]:
- "finite (support_on s f) \<Longrightarrow>
- supp_sum f (insert x s) = (if x \<in> s then supp_sum f s else f x + supp_sum f s)"
+ "finite (support_on S f) \<Longrightarrow>
+ supp_sum f (insert x S) = (if x \<in> S then supp_sum f S else f x + supp_sum f S)"
by (simp add: supp_sum_def in_support_on insert_absorb)
lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A"
@@ -70,17 +70,36 @@
lemma image_affinity_interval:
fixes c :: "'a::ordered_real_vector"
- shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
+ shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) =
+ (if {a..b}={} then {}
+ else if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
else {m *\<^sub>R b + c .. m *\<^sub>R a + c})"
- apply (case_tac "m=0", force)
- apply (auto simp: scaleR_left_mono)
- apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg)
- apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive)
- apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq)
- using le_diff_eq scaleR_le_cancel_left_neg
- apply fastforce
- done
+ (is "?lhs = ?rhs")
+proof (cases "m=0")
+ case True
+ then show ?thesis
+ by force
+next
+ case False
+ show ?thesis
+ proof
+ show "?lhs \<subseteq> ?rhs"
+ by (auto simp: scaleR_left_mono scaleR_left_mono_neg)
+ show "?rhs \<subseteq> ?lhs"
+ proof (clarsimp, intro conjI impI subsetI)
+ show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk>
+ \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
+ apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
+ using False apply (auto simp: le_diff_eq pos_le_divideRI)
+ using diff_le_eq pos_le_divideR_eq by force
+ show "\<lbrakk>\<not> 0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
+ \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
+ apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
+ apply (auto simp: diff_le_eq neg_le_divideR_eq)
+ using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce
+ qed
+ qed
+qed
lemma countable_PiE:
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
@@ -286,78 +305,83 @@
end
lemma (in first_countable_topology) first_countable_basisE:
- obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
- "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
- using first_countable_basis[of x]
- apply atomize_elim
- apply (elim exE)
- apply (rule_tac x="range A" in exI, auto)
- done
+ 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"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> 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 \<A>)"
+ 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"
- "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
- "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
+ obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
+ "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>"
proof atomize_elim
- obtain A' where A':
- "countable A'"
- "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
- "\<And>a. a \<in> A' \<Longrightarrow> open a"
- "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
+ obtain \<B> where \<B>:
+ "countable \<B>"
+ "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B"
+ "\<And>B. B \<in> \<B> \<Longrightarrow> open B"
+ "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S"
by (rule first_countable_basisE) blast
- define A where [abs_def]:
- "A = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
- then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
- (\<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 A"
- unfolding A_def by (intro countable_image countable_Collect_finite)
- fix a
- assume "a \<in> A"
- then show "x \<in> a" "open a"
- using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
+ define \<A> where [abs_def]:
+ "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)"
+ then show "\<exists>\<A>. countable \<A> \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> x \<in> A) \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> open A) \<and>
+ (\<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 \<A>"
+ unfolding \<A>_def by (intro countable_image countable_Collect_finite)
+ fix A
+ assume "A \<in> \<A>"
+ then show "x \<in> A" "open A"
+ using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into)
next
- let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
- fix a b
- assume "a \<in> A" "b \<in> A"
- then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
- by (auto simp: A_def)
- then show "a \<inter> b \<in> A"
- by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
+ let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)"
+ fix A B
+ assume "A \<in> \<A>" "B \<in> \<A>"
+ then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)"
+ by (auto simp: \<A>_def)
+ then show "A \<inter> B \<in> \<A>"
+ by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
next
fix S
assume "open S" "x \<in> S"
- then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
- then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
- by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
+ then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast
+ then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B>
+ 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 A"
- and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
- and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
- shows "\<exists>A::nat \<Rightarrow> '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))"
-proof (safe intro!: exI[of _ "from_nat_into A"])
+ assumes "countable \<A>"
+ and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
+ and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S"
+ shows "\<exists>\<A>::nat \<Rightarrow> '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))"
+proof (safe intro!: exI[of _ "from_nat_into \<A>"])
fix i
- have "A \<noteq> {}" using 2[of UNIV] by auto
- show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
- using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto
+ have "\<A> \<noteq> {}" using 2[of UNIV] by auto
+ show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)"
+ using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
next
fix S
assume "open S" "x\<in>S" from 2[OF this]
- show "\<exists>i. from_nat_into A i \<subseteq> S"
- using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto
+ show "\<exists>i. from_nat_into \<A> i \<subseteq> 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 \<times> 'b"
- obtain A where A:
- "countable A"
- "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
- "\<And>a. a \<in> A \<Longrightarrow> open a"
- "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
+ obtain \<A> where \<A>:
+ "countable \<A>"
+ "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a"
+ "\<And>a. a \<in> \<A> \<Longrightarrow> open a"
+ "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S"
by (rule first_countable_basisE[of "fst x"]) blast
obtain B where B:
"countable B"
@@ -365,27 +389,28 @@
"\<And>a. a \<in> B \<Longrightarrow> open a"
"\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
by (rule first_countable_basisE[of "snd x"]) blast
- show "\<exists>A::nat \<Rightarrow> ('a \<times> '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 "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
+ show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> '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 "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe)
fix a b
- assume x: "a \<in> A" "b \<in> B"
- with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)"
- unfolding mem_Times_iff
- by (auto intro: open_Times)
+ assume x: "a \<in> \<A>" "b \<in> B"
+ show "x \<in> a \<times> b"
+ by (simp add: \<A>(2) B(2) mem_Times_iff x)
+ show "open (a \<times> b)"
+ by (simp add: \<A>(3) B(3) open_Times x)
next
fix S
assume "open S" "x \<in> S"
then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
by (rule open_prod_elim)
moreover
- from a'b' A(4)[of a'] B(4)[of b']
- obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
+ from a'b' \<A>(4)[of a'] B(4)[of b']
+ obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
by auto
ultimately
- show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
+ show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S"
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
- qed (simp add: A B)
+ qed (simp add: \<A> B)
qed
class second_countable_topology = topological_space +
@@ -962,61 +987,60 @@
qed
lemma connected_openin:
- "connected s \<longleftrightarrow>
- ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
- openin (subtopology euclidean s) e2 \<and>
- s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
+ "connected S \<longleftrightarrow>
+ ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
+ openin (subtopology euclidean S) E2 \<and>
+ S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
apply (simp_all, blast+) (* SLOW *)
done
lemma connected_openin_eq:
- "connected s \<longleftrightarrow>
- ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
- openin (subtopology euclidean s) e2 \<and>
- e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
- e1 \<noteq> {} \<and> e2 \<noteq> {})"
+ "connected S \<longleftrightarrow>
+ ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
+ openin (subtopology euclidean S) E2 \<and>
+ E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
+ E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_openin, safe, blast)
by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
lemma connected_closedin:
- "connected s \<longleftrightarrow>
- ~(\<exists>e1 e2.
- closedin (subtopology euclidean s) e1 \<and>
- closedin (subtopology euclidean s) e2 \<and>
- s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and>
- e1 \<noteq> {} \<and> e2 \<noteq> {})"
-proof -
- { fix A B x x'
- assume s_sub: "s \<subseteq> A \<union> B"
- and disj: "A \<inter> B \<inter> s = {}"
- and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A"
- and cl: "closed A" "closed B"
- assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})"
- then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D"
- by (metis (no_types) Int_Un_distrib Int_assoc)
- moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}"
- using disj s_sub x by blast+
- ultimately have "s \<inter> A = {}"
- using cl by (metis inf.left_commute inf_bot_right order_refl)
- then have False
- using x' by blast
- } note * = this
- show ?thesis
- apply (simp add: connected_closed closedin_closed)
- apply (safe; simp)
- apply blast
- apply (blast intro: *)
- done
+ "connected S \<longleftrightarrow>
+ (\<nexists>E1 E2.
+ closedin (subtopology euclidean S) E1 \<and>
+ closedin (subtopology euclidean S) E2 \<and>
+ S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (auto simp add: connected_closed closedin_closed)
+next
+ assume R: ?rhs
+ then show ?lhs
+ proof (clarsimp simp add: connected_closed closedin_closed)
+ fix A B
+ assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
+ and disj: "A \<inter> B \<inter> S = {}"
+ and cl: "closed A" "closed B"
+ have "S \<inter> (A \<union> B) = S"
+ using s_sub(1) by auto
+ have "S - A = B \<inter> S"
+ using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
+ then have "S \<inter> A = {}"
+ by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
+ then show "A \<inter> S = {}"
+ by blast
+ qed
qed
lemma connected_closedin_eq:
- "connected s \<longleftrightarrow>
- ~(\<exists>e1 e2.
- closedin (subtopology euclidean s) e1 \<and>
- closedin (subtopology euclidean s) e2 \<and>
- e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
- e1 \<noteq> {} \<and> e2 \<noteq> {})"
+ "connected S \<longleftrightarrow>
+ ~(\<exists>E1 E2.
+ closedin (subtopology euclidean S) E1 \<and>
+ closedin (subtopology euclidean S) E2 \<and>
+ E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
+ E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_closedin, safe, blast)
by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
@@ -1662,100 +1686,48 @@
and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
proof -
- show ?th1
- unfolding subset_eq and Ball_def and mem_box
- by (auto intro: order_trans)
- show ?th2
- unfolding subset_eq and Ball_def and mem_box
- by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
- {
- assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
- then have "box c d \<noteq> {}"
- unfolding box_eq_empty by auto
- fix i :: 'a
- assume i: "i \<in> Basis"
- (** TODO combine the following two parts as done in the HOL_light version. **)
- {
- let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
- assume as2: "a\<bullet>i > c\<bullet>i"
- {
- fix j :: 'a
- assume j: "j \<in> Basis"
- then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
- apply (cases "j = i")
- using as(2)[THEN bspec[where x=j]] i
- apply (auto simp: as2)
- done
- }
- then have "?x\<in>box c d"
- using i unfolding mem_box by auto
- moreover
- have "?x \<notin> cbox a b"
- unfolding mem_box
- apply auto
- apply (rule_tac x=i in bexI)
- using as(2)[THEN bspec[where x=i]] and as2 i
- apply auto
- done
- ultimately have False using as by auto
+ let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+ let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
+ show ?th1 ?th2
+ by (fastforce simp: mem_box)+
+ have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
+ if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
+ proof -
+ have "box c d \<noteq> {}"
+ using that
+ unfolding box_eq_empty by force
+ { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
+ assume *: "a\<bullet>i > c\<bullet>i"
+ then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
+ using cd that by (fastforce simp add: i *)
+ then have "?x \<in> box c d"
+ unfolding mem_box by auto
+ moreover have "?x \<notin> cbox a b"
+ using i cd * by (force simp: mem_box)
+ ultimately have False using box by auto
}
- then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
+ then have "a\<bullet>i \<le> c\<bullet>i" by force
moreover
- {
- let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
- assume as2: "b\<bullet>i < d\<bullet>i"
- {
- fix j :: 'a
- assume "j\<in>Basis"
- then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
- apply (cases "j = i")
- using as(2)[THEN bspec[where x=j]]
- apply (auto simp: as2)
- done
- }
- then have "?x\<in>box c d"
+ { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
+ assume *: "b\<bullet>i < d\<bullet>i"
+ then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
+ using cd that by (fastforce simp add: i *)
+ then have "?x \<in> box c d"
unfolding mem_box by auto
- moreover
- have "?x\<notin>cbox a b"
- unfolding mem_box
- apply auto
- apply (rule_tac x=i in bexI)
- using as(2)[THEN bspec[where x=i]] and as2 using i
- apply auto
- done
- ultimately have False using as by auto
+ moreover have "?x \<notin> cbox a b"
+ using i cd * by (force simp: mem_box)
+ ultimately have False using box by auto
}
then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
- ultimately
- have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
- } note part1 = this
+ ultimately show ?thesis by auto
+ qed
show ?th3
- unfolding subset_eq and Ball_def and mem_box
- apply (rule, rule, rule, rule)
- apply (rule part1)
- unfolding subset_eq and Ball_def and mem_box
- prefer 4
- apply auto
- apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
- done
- {
- assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
- fix i :: 'a
- assume i:"i\<in>Basis"
- from as(1) have "box c d \<subseteq> cbox a b"
- using box_subset_cbox[of a b] by auto
- then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
- using part1 and as(2) using i by auto
- } note * = this
+ using acdb by (fastforce simp add: mem_box)
+ have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
+ if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
+ using box_subset_cbox[of a b] that acdb by auto
show ?th4
- unfolding subset_eq and Ball_def and mem_box
- apply (rule, rule, rule, rule)
- apply (rule *)
- unfolding subset_eq and Ball_def and mem_box
- prefer 4
- apply auto
- apply (erule_tac x=xa in allE, simp)+
- done
+ using acdb' by (fastforce simp add: mem_box)
qed
lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
@@ -1775,19 +1747,14 @@
lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume ?lhs
- then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b"
+ assume L: ?lhs
+ then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
by auto
then show ?rhs
apply (simp add: subset_box)
- using \<open>cbox a b = box c d\<close> box_ne_empty box_sing
- apply (fastforce simp add:)
+ using L box_ne_empty box_sing apply (fastforce simp add:)
done
-next
- assume ?rhs
- then show ?lhs
- by force
-qed
+qed force
lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
by (metis eq_cbox_box)
@@ -1795,20 +1762,16 @@
lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume ?lhs
+ assume L: ?lhs
then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
by auto
then show ?rhs
apply (simp add: subset_box)
- using box_ne_empty(2) \<open>box a b = box c d\<close>
+ using box_ne_empty(2) L
apply auto
apply (meson euclidean_eqI less_eq_real_def not_less)+
done
-next
- assume ?rhs
- then show ?lhs
- by force
-qed
+qed force
lemma subset_box_complex:
"cbox a b \<subseteq> cbox c d \<longleftrightarrow>
@@ -2140,7 +2103,7 @@
and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
shows "closed S"
proof -
- have False if C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
+ have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
proof -
from e have e2: "e/2 > 0" by arith
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
@@ -2148,7 +2111,7 @@
let ?m = "min (e/2) (dist x y) "
from e2 y(2) have mp: "?m > 0"
by simp
- from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
+ from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
by blast
from z y have "dist z y < e"
by (intro dist_triangle_lt [where z=x]) simp
@@ -2991,9 +2954,9 @@
assume "m < n"
have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
by simp
- also have "... < dist (f n) x"
+ also have "\<dots> < dist (f n) x"
by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
- also have "... < dist (f m) x"
+ also have "\<dots> < dist (f m) x"
using Suc.IH \<open>m < n\<close> by blast
finally show ?thesis .
next
@@ -3127,9 +3090,9 @@
proof -
have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B"
by (simp add: mult_left_mono g)
- also have "... \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
+ also have "\<dots> \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
by (simp add: mult_left_mono)
- also have "... < \<epsilon>"
+ also have "\<dots> < \<epsilon>"
by (rule f)
finally show ?thesis .
qed
@@ -3290,7 +3253,7 @@
lemma closure_approachableD:
assumes "x \<in> closure S" "e>0"
shows "\<exists>y\<in>S. dist x y < e"
- using assms unfolding closure_approachable by (auto simp add: dist_commute)
+ using assms unfolding closure_approachable by (auto simp: dist_commute)
lemma closed_approachable:
fixes S :: "'a::metric_space set"
@@ -5262,9 +5225,9 @@
shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
proof -
have *: "filterlim x (inf (nhds a) (principal s)) F"
- using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp add: filterlim_principal eventually_mono)
+ using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono)
show ?thesis
- by (auto simp add: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
+ by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
qed
lemma continuous_within_tendsto_compose':
@@ -5402,7 +5365,7 @@
lemma continuous_closed_imp_Cauchy_continuous:
fixes S :: "('a::complete_space) set"
- shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
+ shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
by (meson LIMSEQ_imp_Cauchy complete_def)
@@ -5876,30 +5839,20 @@
let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
{
fix x :: "'a"
- assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
- {
- fix i :: 'a
- assume "i \<in> Basis"
- then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
- using x[THEN bspec[where x=i]] by auto
- }
+ assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
- apply -
- apply (rule sum_mono, auto)
- done
+ by (force simp: intro!: sum_mono)
then have "norm x \<le> ?b"
using norm_le_l1[of x] by auto
}
then show ?thesis
- unfolding cbox_def bounded_iff by auto
+ unfolding cbox_def bounded_iff by force
qed
lemma bounded_box [simp]:
fixes a :: "'a::euclidean_space"
shows "bounded (box a b)"
- using bounded_cbox[of a b]
- using box_subset_cbox[of a b]
- using bounded_subset[of "cbox a b" "box a b"]
+ using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
by simp
lemma not_interval_UNIV [simp]:
@@ -5923,12 +5876,8 @@
assumes "box a b \<noteq> {}"
shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
proof -
- {
- fix i :: 'a
- assume "i \<in> Basis"
- then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
- using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
- }
+ have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
+ using assms that by (auto simp: inner_add_left box_ne_empty)
then show ?thesis unfolding mem_box by auto
qed
@@ -5945,14 +5894,12 @@
have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
unfolding left_diff_distrib by simp
also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
- apply (rule add_less_le_mono)
- using e unfolding mult_less_cancel_left and mult_le_cancel_left
- apply simp_all
- using x unfolding mem_box using i
- apply simp
- using y unfolding mem_box using i
- apply simp
- done
+ proof (rule add_less_le_mono)
+ show "e * (a \<bullet> i) < e * (x \<bullet> i)"
+ using \<open>0 < e\<close> i mem_box(1) x by auto
+ show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
+ by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
+ qed
finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
unfolding inner_simps by auto
moreover
@@ -5962,9 +5909,9 @@
also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
proof (rule add_less_le_mono)
show "e * (x \<bullet> i) < e * (b \<bullet> i)"
- using e(1) i mem_box(1) x by auto
+ using \<open>0 < e\<close> i mem_box(1) x by auto
show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
- by (meson diff_ge_0_iff_ge e(2) i mem_box(2) ordered_comm_semiring_class.comm_mult_left_mono y)
+ by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
qed
finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
unfolding inner_simps by auto
@@ -6011,13 +5958,8 @@
{
fix e :: real
assume "e > 0"
- then have "\<exists>N::nat. inverse (real (N + 1)) < e"
- using real_arch_inverse[of e]
- apply (auto simp: Suc_pred')
- apply (metis Suc_pred' of_nat_Suc)
- done
then obtain N :: nat where N: "inverse (real (N + 1)) < e"
- by auto
+ using reals_Archimedean by auto
have "inverse (real n + 1) < e" if "N \<le> n" for n
by (auto intro!: that le_less_trans [OF _ N])
then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
@@ -6031,9 +5973,8 @@
by auto
}
ultimately have "x \<in> closure (box a b)"
- using as and box_midpoint[OF assms]
- unfolding closure_def
- unfolding islimpt_sequential
+ using as box_midpoint[OF assms]
+ unfolding closure_def islimpt_sequential
by (cases "x=?c") (auto simp: in_box_eucl_less)
}
then show ?thesis
@@ -6041,49 +5982,31 @@
qed
lemma bounded_subset_box_symmetric:
- fixes s::"('a::euclidean_space) set"
- assumes "bounded s"
- shows "\<exists>a. s \<subseteq> box (-a) a"
+ fixes S :: "('a::euclidean_space) set"
+ assumes "bounded S"
+ obtains a where "S \<subseteq> box (-a) a"
proof -
- obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
+ obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
using assms[unfolded bounded_pos] by auto
define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
- {
- fix x
- assume "x \<in> s"
- fix i :: 'a
- assume i: "i \<in> Basis"
- then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
- using b[THEN bspec[where x=x], OF \<open>x\<in>s\<close>]
- using Basis_le_norm[OF i, of x]
- unfolding inner_simps and a_def
- by auto
- }
- then show ?thesis
- by (auto intro: exI[where x=a] simp add: box_def)
+ have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i
+ using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
+ then have "S \<subseteq> box (-a) a"
+ by (auto simp: simp add: box_def)
+ then show ?thesis ..
qed
-lemma bounded_subset_open_interval:
- fixes s :: "('a::euclidean_space) set"
- shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
- by (auto dest!: bounded_subset_box_symmetric)
-
lemma bounded_subset_cbox_symmetric:
- fixes s :: "('a::euclidean_space) set"
- assumes "bounded s"
- shows "\<exists>a. s \<subseteq> cbox (-a) a"
+ fixes S :: "('a::euclidean_space) set"
+ assumes "bounded S"
+ obtains a where "S \<subseteq> cbox (-a) a"
proof -
- obtain a where "s \<subseteq> box (-a) a"
+ obtain a where "S \<subseteq> box (-a) a"
using bounded_subset_box_symmetric[OF assms] by auto
then show ?thesis
- using box_subset_cbox[of "-a" a] by auto
+ by (meson box_subset_cbox dual_order.trans that)
qed
-lemma bounded_subset_cbox:
- fixes s :: "('a::euclidean_space) set"
- shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
- using bounded_subset_cbox_symmetric[of s] by auto
-
lemma frontier_cbox:
fixes a b :: "'a::euclidean_space"
shows "frontier (cbox a b) = cbox a b - box a b"
@@ -6113,13 +6036,12 @@
lemma eucl_less_eq_halfspaces:
fixes a :: "'a::euclidean_space"
shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
- "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+ "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
by (auto simp: eucl_less_def)
lemma open_Collect_eucl_less[simp, intro]:
fixes a :: "'a::euclidean_space"
- shows "open {x. x <e a}"
- "open {x. a <e x}"
+ shows "open {x. x <e a}" "open {x. a <e x}"
by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
no_notation
--- a/src/HOL/Probability/Fin_Map.thy Tue May 08 21:26:10 2018 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Tue May 08 21:03:06 2018 +0100
@@ -203,7 +203,7 @@
have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)"
show "\<exists>A::nat \<Rightarrow> ('a\<Rightarrow>\<^sub>F'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[where A="?A"], safe)
+ proof (rule first_countableI[of "?A"], safe)
show "countable ?A" using A by (simp add: countable_PiE)
next
fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S"