1.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun Sep 16 16:31:56 2018 +0200
1.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun Sep 16 17:58:59 2018 +0100
1.3 @@ -231,6 +231,16 @@
1.4 and is_interval_cc: "is_interval {b..a}"
1.5 by (force simp: is_interval_def eucl_le[where 'a='a])+
1.6
1.7 +lemma connected_interval [simp]:
1.8 + fixes a b::"'a::ordered_euclidean_space"
1.9 + shows "connected {a..b}"
1.10 + using is_interval_cc is_interval_connected by blast
1.11 +
1.12 +lemma path_connected_interval [simp]:
1.13 + fixes a b::"'a::ordered_euclidean_space"
1.14 + shows "path_connected {a..b}"
1.15 + using is_interval_cc is_interval_path_connected by blast
1.16 +
1.17 lemma%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
1.18 by (auto simp: real_atLeastGreaterThan_eq)
1.19
2.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Sep 16 16:31:56 2018 +0200
2.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Sep 16 17:58:59 2018 +0100
2.3 @@ -700,6 +700,10 @@
2.4 assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
2.5 by (metis (full_types) assms openin_INT2 image_ident)
2.6
2.7 +lemma openin_Int_Inter:
2.8 + assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
2.9 + using openin_Inter [of "insert U \<F>"] assms by auto
2.10 +
2.11
2.12 subsubsection \<open>Closed sets\<close>
2.13
2.14 @@ -824,6 +828,26 @@
2.15 unfolding openin_subtopology
2.16 by auto (metis IntD1 in_mono openin_subset)
2.17
2.18 +lemma subtopology_subtopology:
2.19 + "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
2.20 +proof -
2.21 + have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
2.22 + by (metis inf_assoc)
2.23 + have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
2.24 + by (simp add: subtopology_def)
2.25 + also have "\<dots> = subtopology X (S \<inter> T)"
2.26 + by (simp add: openin_subtopology eq) (simp add: subtopology_def)
2.27 + finally show ?thesis .
2.28 +qed
2.29 +
2.30 +lemma openin_subtopology_alt:
2.31 + "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
2.32 + by (simp add: image_iff inf_commute openin_subtopology)
2.33 +
2.34 +lemma closedin_subtopology_alt:
2.35 + "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
2.36 + by (simp add: image_iff inf_commute closedin_subtopology)
2.37 +
2.38 lemma subtopology_superset:
2.39 assumes UV: "topspace U \<subseteq> V"
2.40 shows "subtopology U V = U"
2.41 @@ -869,6 +893,9 @@
2.42 "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
2.43 by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
2.44
2.45 +lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
2.46 + by (simp add: closedin_def)
2.47 +
2.48 lemma openin_imp_subset:
2.49 "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
2.50 by (metis Int_iff openin_subtopology subsetI)
2.51 @@ -877,6 +904,14 @@
2.52 "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
2.53 by (simp add: closedin_def topspace_subtopology)
2.54
2.55 +lemma openin_open_subtopology:
2.56 + "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
2.57 + by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
2.58 +
2.59 +lemma closedin_closed_subtopology:
2.60 + "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
2.61 + by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
2.62 +
2.63 lemma openin_subtopology_Un:
2.64 "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
2.65 \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
3.1 --- a/src/HOL/Library/FuncSet.thy Sun Sep 16 16:31:56 2018 +0200
3.2 +++ b/src/HOL/Library/FuncSet.thy Sun Sep 16 17:58:59 2018 +0100
3.3 @@ -499,6 +499,41 @@
3.4 shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E T"
3.5 using assms unfolding extensional_funcset_def extensional_def by auto
3.6
3.7 +lemma subset_PiE:
3.8 + "PiE I S \<subseteq> PiE I T \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. S i \<subseteq> T i)" (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
3.9 +proof (cases "PiE I S = {}")
3.10 + case False
3.11 + moreover have "?lhs = ?rhs"
3.12 + proof
3.13 + assume L: ?lhs
3.14 + have "\<And>i. i\<in>I \<Longrightarrow> S i \<noteq> {}"
3.15 + using False PiE_eq_empty_iff by blast
3.16 + with L show ?rhs
3.17 + by (simp add: PiE_Int PiE_eq_iff inf.absorb_iff2)
3.18 + qed auto
3.19 + ultimately show ?thesis
3.20 + by simp
3.21 +qed simp
3.22 +
3.23 +lemma PiE_eq:
3.24 + "PiE I S = PiE I T \<longleftrightarrow> PiE I S = {} \<and> PiE I T = {} \<or> (\<forall>i \<in> I. S i = T i)"
3.25 + by (auto simp: PiE_eq_iff PiE_eq_empty_iff)
3.26 +
3.27 +lemma PiE_UNIV [simp]: "PiE UNIV (\<lambda>i. UNIV) = UNIV"
3.28 + by blast
3.29 +
3.30 +lemma image_projection_PiE:
3.31 + "(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
3.32 +proof -
3.33 + have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
3.34 + using that apply auto
3.35 + by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
3.36 + moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
3.37 + using that by (blast intro: PiE_arb [OF that, symmetric])
3.38 + ultimately show ?thesis
3.39 + by auto
3.40 +qed
3.41 +
3.42
3.43 subsubsection \<open>Injective Extensional Function Spaces\<close>
3.44
4.1 --- a/src/HOL/Zorn.thy Sun Sep 16 16:31:56 2018 +0200
4.2 +++ b/src/HOL/Zorn.thy Sun Sep 16 17:58:59 2018 +0100
4.3 @@ -386,7 +386,7 @@
4.4 subsubsection \<open>Zorn's lemma\<close>
4.5
4.6 text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
4.7 -lemma subset_Zorn:
4.8 +theorem subset_Zorn:
4.9 assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
4.10 shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
4.11 proof -
4.12 @@ -487,7 +487,7 @@
4.13 lemma Zorn_Lemma2: "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
4.14 using subset_Zorn [of A] by (auto simp: chains_alt_def)
4.15
4.16 -text \<open>Various other lemmas\<close>
4.17 +subsection \<open>Other variants of Zorn's Lemma\<close>
4.18
4.19 lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
4.20 unfolding chains_def chain_subset_def by blast
4.21 @@ -562,6 +562,67 @@
4.22 by (auto simp: relation_of_def)
4.23 qed
4.24
4.25 +lemma Union_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Union>\<B> \<in> \<B>"
4.26 +proof (induction \<B> rule: finite_induct)
4.27 + case (insert B \<B>)
4.28 + show ?case
4.29 + proof (cases "\<B> = {}")
4.30 + case False
4.31 + then show ?thesis
4.32 + using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Union>\<B>"])
4.33 + qed auto
4.34 +qed simp
4.35 +
4.36 +lemma Inter_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Inter>\<B> \<in> \<B>"
4.37 +proof (induction \<B> rule: finite_induct)
4.38 + case (insert B \<B>)
4.39 + show ?case
4.40 + proof (cases "\<B> = {}")
4.41 + case False
4.42 + then show ?thesis
4.43 + using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Inter>\<B>"])
4.44 + qed auto
4.45 +qed simp
4.46 +
4.47 +lemma finite_subset_Union_chain:
4.48 + assumes "finite A" "A \<subseteq> \<Union>\<B>" "\<B> \<noteq> {}" and sub: "subset.chain \<A> \<B>"
4.49 + obtains B where "B \<in> \<B>" "A \<subseteq> B"
4.50 +proof -
4.51 + obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
4.52 + using assms by (auto intro: finite_subset_Union)
4.53 + show thesis
4.54 + proof (cases "\<F> = {}")
4.55 + case True
4.56 + then show ?thesis
4.57 + using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
4.58 + next
4.59 + case False
4.60 + show ?thesis
4.61 + proof
4.62 + show "\<Union>\<F> \<in> \<B>"
4.63 + using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
4.64 + by (simp add: Union_in_chain False subset.chain_def subset_iff)
4.65 + show "A \<subseteq> \<Union>\<F>"
4.66 + using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
4.67 + qed
4.68 + qed
4.69 +qed
4.70 +
4.71 +lemma subset_Zorn_nonempty:
4.72 + assumes "\<A> \<noteq> {}" and ch: "\<And>\<C>. \<lbrakk>\<C>\<noteq>{}; subset.chain \<A> \<C>\<rbrakk> \<Longrightarrow> \<Union>\<C> \<in> \<A>"
4.73 + shows "\<exists>M\<in>\<A>. \<forall>X\<in>\<A>. M \<subseteq> X \<longrightarrow> X = M"
4.74 +proof (rule subset_Zorn)
4.75 + show "\<exists>U\<in>\<A>. \<forall>X\<in>\<C>. X \<subseteq> U" if "subset.chain \<A> \<C>" for \<C>
4.76 + proof (cases "\<C> = {}")
4.77 + case True
4.78 + then show ?thesis
4.79 + using \<open>\<A> \<noteq> {}\<close> by blast
4.80 + next
4.81 + case False
4.82 + show ?thesis
4.83 + by (blast intro!: ch False that Union_upper)
4.84 + qed
4.85 +qed
4.86
4.87 subsection \<open>The Well Ordering Theorem\<close>
4.88