--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun Sep 16 17:58:59 2018 +0100
@@ -231,6 +231,16 @@
and is_interval_cc: "is_interval {b..a}"
by (force simp: is_interval_def eucl_le[where 'a='a])+
+lemma connected_interval [simp]:
+ fixes a b::"'a::ordered_euclidean_space"
+ shows "connected {a..b}"
+ using is_interval_cc is_interval_connected by blast
+
+lemma path_connected_interval [simp]:
+ fixes a b::"'a::ordered_euclidean_space"
+ shows "path_connected {a..b}"
+ using is_interval_cc is_interval_path_connected by blast
+
lemma%unimportant is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
by (auto simp: real_atLeastGreaterThan_eq)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Sep 16 17:58:59 2018 +0100
@@ -700,6 +700,10 @@
assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
by (metis (full_types) assms openin_INT2 image_ident)
+lemma openin_Int_Inter:
+ assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
+ using openin_Inter [of "insert U \<F>"] assms by auto
+
subsubsection \<open>Closed sets\<close>
@@ -824,6 +828,26 @@
unfolding openin_subtopology
by auto (metis IntD1 in_mono openin_subset)
+lemma subtopology_subtopology:
+ "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
+proof -
+ 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)"
+ by (metis inf_assoc)
+ have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
+ by (simp add: subtopology_def)
+ also have "\<dots> = subtopology X (S \<inter> T)"
+ by (simp add: openin_subtopology eq) (simp add: subtopology_def)
+ finally show ?thesis .
+qed
+
+lemma openin_subtopology_alt:
+ "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
+ by (simp add: image_iff inf_commute openin_subtopology)
+
+lemma closedin_subtopology_alt:
+ "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
+ by (simp add: image_iff inf_commute closedin_subtopology)
+
lemma subtopology_superset:
assumes UV: "topspace U \<subseteq> V"
shows "subtopology U V = U"
@@ -869,6 +893,9 @@
"closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
+lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
+ by (simp add: closedin_def)
+
lemma openin_imp_subset:
"openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (metis Int_iff openin_subtopology subsetI)
@@ -877,6 +904,14 @@
"closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (simp add: closedin_def topspace_subtopology)
+lemma openin_open_subtopology:
+ "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
+ by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
+
+lemma closedin_closed_subtopology:
+ "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
+ by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
+
lemma openin_subtopology_Un:
"\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
\<Longrightarrow> openin (subtopology X (T \<union> U)) S"
--- a/src/HOL/Library/FuncSet.thy Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy Sun Sep 16 17:58:59 2018 +0100
@@ -499,6 +499,41 @@
shows "f(x := a) \<in> insert x S \<rightarrow>\<^sub>E T"
using assms unfolding extensional_funcset_def extensional_def by auto
+lemma subset_PiE:
+ "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")
+proof (cases "PiE I S = {}")
+ case False
+ moreover have "?lhs = ?rhs"
+ proof
+ assume L: ?lhs
+ have "\<And>i. i\<in>I \<Longrightarrow> S i \<noteq> {}"
+ using False PiE_eq_empty_iff by blast
+ with L show ?rhs
+ by (simp add: PiE_Int PiE_eq_iff inf.absorb_iff2)
+ qed auto
+ ultimately show ?thesis
+ by simp
+qed simp
+
+lemma PiE_eq:
+ "PiE I S = PiE I T \<longleftrightarrow> PiE I S = {} \<and> PiE I T = {} \<or> (\<forall>i \<in> I. S i = T i)"
+ by (auto simp: PiE_eq_iff PiE_eq_empty_iff)
+
+lemma PiE_UNIV [simp]: "PiE UNIV (\<lambda>i. UNIV) = UNIV"
+ by blast
+
+lemma image_projection_PiE:
+ "(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
+proof -
+ have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
+ using that apply auto
+ by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
+ moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
+ using that by (blast intro: PiE_arb [OF that, symmetric])
+ ultimately show ?thesis
+ by auto
+qed
+
subsubsection \<open>Injective Extensional Function Spaces\<close>
--- a/src/HOL/Zorn.thy Sun Sep 16 16:31:56 2018 +0200
+++ b/src/HOL/Zorn.thy Sun Sep 16 17:58:59 2018 +0100
@@ -386,7 +386,7 @@
subsubsection \<open>Zorn's lemma\<close>
text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
-lemma subset_Zorn:
+theorem subset_Zorn:
assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
proof -
@@ -487,7 +487,7 @@
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"
using subset_Zorn [of A] by (auto simp: chains_alt_def)
-text \<open>Various other lemmas\<close>
+subsection \<open>Other variants of Zorn's Lemma\<close>
lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
unfolding chains_def chain_subset_def by blast
@@ -562,6 +562,67 @@
by (auto simp: relation_of_def)
qed
+lemma Union_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Union>\<B> \<in> \<B>"
+proof (induction \<B> rule: finite_induct)
+ case (insert B \<B>)
+ show ?case
+ proof (cases "\<B> = {}")
+ case False
+ then show ?thesis
+ using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Union>\<B>"])
+ qed auto
+qed simp
+
+lemma Inter_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Inter>\<B> \<in> \<B>"
+proof (induction \<B> rule: finite_induct)
+ case (insert B \<B>)
+ show ?case
+ proof (cases "\<B> = {}")
+ case False
+ then show ?thesis
+ using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Inter>\<B>"])
+ qed auto
+qed simp
+
+lemma finite_subset_Union_chain:
+ assumes "finite A" "A \<subseteq> \<Union>\<B>" "\<B> \<noteq> {}" and sub: "subset.chain \<A> \<B>"
+ obtains B where "B \<in> \<B>" "A \<subseteq> B"
+proof -
+ obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
+ using assms by (auto intro: finite_subset_Union)
+ show thesis
+ proof (cases "\<F> = {}")
+ case True
+ then show ?thesis
+ using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
+ next
+ case False
+ show ?thesis
+ proof
+ show "\<Union>\<F> \<in> \<B>"
+ using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
+ by (simp add: Union_in_chain False subset.chain_def subset_iff)
+ show "A \<subseteq> \<Union>\<F>"
+ using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
+ qed
+ qed
+qed
+
+lemma subset_Zorn_nonempty:
+ assumes "\<A> \<noteq> {}" and ch: "\<And>\<C>. \<lbrakk>\<C>\<noteq>{}; subset.chain \<A> \<C>\<rbrakk> \<Longrightarrow> \<Union>\<C> \<in> \<A>"
+ shows "\<exists>M\<in>\<A>. \<forall>X\<in>\<A>. M \<subseteq> X \<longrightarrow> X = M"
+proof (rule subset_Zorn)
+ show "\<exists>U\<in>\<A>. \<forall>X\<in>\<C>. X \<subseteq> U" if "subset.chain \<A> \<C>" for \<C>
+ proof (cases "\<C> = {}")
+ case True
+ then show ?thesis
+ using \<open>\<A> \<noteq> {}\<close> by blast
+ next
+ case False
+ show ?thesis
+ by (blast intro!: ch False that Union_upper)
+ qed
+qed
subsection \<open>The Well Ordering Theorem\<close>