Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Set_Idioms.thy Sprache: Isabelle

Original von: Isabelle^©

(* Title: HOL/Library/Set_Idioms.thy
 Author: Lawrence Paulson (but borrowed from HOL Light)
*)

section \<open>Set Idioms\<close>

theory Set_Idioms
imports Countable_Set

begin

subsection\<open>Idioms for being a suitable union/intersection of something\<close>

definition union_of :: "('a set set \ bool) \ ('a set \ bool) \ 'a set \ bool"
 (infixr "union'_of" 60)
 where "P union_of Q \ \S. \\. P \ \ \ \ Collect Q \ \\ = S"

definition intersection_of :: "('a set set \ bool) \ ('a set \ bool) \ 'a set \ bool"
 (infixr "intersection'_of" 60)
 where "P intersection_of Q \ \S. \\. P \ \ \ \ Collect Q \ \\ = S"

definition arbitrary:: "'a set set \ bool" where "arbitrary \ \ True"

lemma union_of_inc: "\P {S}; Q S\ \ (P union_of Q) S"
 by (auto simp: union_of_def)

lemma intersection_of_inc:
 "\P {S}; Q S\ \ (P intersection_of Q) S"
 by (auto simp: intersection_of_def)

lemma union_of_mono:
 "\(P union_of Q) S; \x. Q x \ Q' x\ \ (P union_of Q') S"
 by (auto simp: union_of_def)

lemma intersection_of_mono:
 "\(P intersection_of Q) S; \x. Q x \ Q' x\ \ (P intersection_of Q') S"
 by (auto simp: intersection_of_def)

lemma all_union_of:
 "(\S. (P union_of Q) S \ R S) \ (\T. P T \ T \ Collect Q \ R(\T))"
 by (auto simp: union_of_def)

lemma all_intersection_of:
 "(\S. (P intersection_of Q) S \ R S) \ (\T. P T \ T \ Collect Q \ R(\T))"
 by (auto simp: intersection_of_def)

lemma intersection_ofE:
 "\(P intersection_of Q) S; \T. \P T; T \ Collect Q\ \ R(\T)\ \ R S"
 by (auto simp: intersection_of_def)

lemma union_of_empty:
 "P {} \ (P union_of Q) {}"
 by (auto simp: union_of_def)

lemma intersection_of_empty:
 "P {} \ (P intersection_of Q) UNIV"
 by (auto simp: intersection_of_def)

text\<open> The arbitrary and finite cases\<close>

lemma arbitrary_union_of_alt:
 "(arbitrary union_of Q) S \ (\x \ S. \U. Q U \ x \ U \ U \ S)"
(is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 by (force simp: union_of_def arbitrary_def)
next
 assume ?rhs
 then have "{U. Q U \ U \ S} \ Collect Q" "\{U. Q U \ U \ S} = S"
 by auto
 then show ?lhs
 unfolding union_of_def arbitrary_def by blast
qed

lemma arbitrary_union_of_empty [simp]: "(arbitrary union_of P) {}"
 by (force simp: union_of_def arbitrary_def)

lemma arbitrary_intersection_of_empty [simp]:
 "(arbitrary intersection_of P) UNIV"
 by (force simp: intersection_of_def arbitrary_def)

lemma arbitrary_union_of_inc:
 "P S \ (arbitrary union_of P) S"
 by (force simp: union_of_inc arbitrary_def)

lemma arbitrary_intersection_of_inc:
 "P S \ (arbitrary intersection_of P) S"
 by (force simp: intersection_of_inc arbitrary_def)

lemma arbitrary_union_of_complement:
 "(arbitrary union_of P) S \ (arbitrary intersection_of (\S. P(- S))) (- S)" (is "?lhs = ?rhs")
proof
 assume ?lhs
 then obtain \ where "\ \<subseteq> Collect P" "S = \<Union>\"
 by (auto simp: union_of_def arbitrary_def)
 then show ?rhs
 unfolding intersection_of_def arbitrary_def
 by (rule_tac x="uminus ` \" in exI) auto
next
 assume ?rhs
 then obtain \ where "\ \<subseteq> {S. P (- S)}" "\<Inter>\ = - S"
 by (auto simp: union_of_def intersection_of_def arbitrary_def)
 then show ?lhs
 unfolding union_of_def arbitrary_def
 by (rule_tac x="uminus ` \" in exI) auto
qed

lemma arbitrary_intersection_of_complement:
 "(arbitrary intersection_of P) S \ (arbitrary union_of (\S. P(- S))) (- S)"
 by (simp add: arbitrary_union_of_complement)

lemma arbitrary_union_of_idempot [simp]:
 "arbitrary union_of arbitrary union_of P = arbitrary union_of P"
proof -
 have 1: "\\'\Collect P. \\' = \\" if "\ \ {S. \\\Collect P. \\ = S}" for \
 proof -
 let ?\<W> = "{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \. \<Union>\<V> = S)}"
 have *: "\x U. \x \ U; U \ \\ \ x \ \?\"
 using that
 apply simp
 apply (drule subsetD, assumption, auto)
 done
 show ?thesis
 apply (rule_tac x="{V. \\. \\Collect P \ V \ \ \ (\S \ \. \\ = S)}" in exI)
 using that by (blast intro: *)
 qed
 have 2: "\\'\{S. \\\Collect P. \\ = S}. \\' = \\" if "\ \ Collect P" for \
 by (metis (mono_tags, lifting) union_of_def arbitrary_union_of_inc that)
 show ?thesis
 unfolding union_of_def arbitrary_def by (force simp: 1 2)
qed

lemma arbitrary_intersection_of_idempot:
 "arbitrary intersection_of arbitrary intersection_of P = arbitrary intersection_of P" (is "?lhs = ?rhs")
proof -
 have "- ?lhs = - ?rhs"
 unfolding arbitrary_intersection_of_complement by simp
 then show ?thesis
 by simp
qed

lemma arbitrary_union_of_Union:
 "(\S. S \ \ \ (arbitrary union_of P) S) \ (arbitrary union_of P) (\\)"
 by (metis union_of_def arbitrary_def arbitrary_union_of_idempot mem_Collect_eq subsetI)

lemma arbitrary_union_of_Un:
 "\(arbitrary union_of P) S; (arbitrary union_of P) T\
 \<Longrightarrow> (arbitrary union_of P) (S \<union> T)"
 using arbitrary_union_of_Union [of "{S,T}"] by auto

lemma arbitrary_intersection_of_Inter:
 "(\S. S \ \ \ (arbitrary intersection_of P) S) \ (arbitrary intersection_of P) (\\)"
 by (metis intersection_of_def arbitrary_def arbitrary_intersection_of_idempot mem_Collect_eq subsetI)

lemma arbitrary_intersection_of_Int:
 "\(arbitrary intersection_of P) S; (arbitrary intersection_of P) T\
 \<Longrightarrow> (arbitrary intersection_of P) (S \<inter> T)"
 using arbitrary_intersection_of_Inter [of "{S,T}"] by auto

lemma arbitrary_union_of_Int_eq:
 "(\S T. (arbitrary union_of P) S \ (arbitrary union_of P) T
 \<longrightarrow> (arbitrary union_of P) (S \<inter> T))
 \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))" (is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 by (simp add: arbitrary_union_of_inc)
next
 assume R: ?rhs
 show ?lhs
 proof clarify
 fix S :: "'a set" and T :: "'a set"
 assume "(arbitrary union_of P) S" and "(arbitrary union_of P) T"
 then obtain \ \<V> where *: "\ \<subseteq> Collect P" "\<Union>\ = S" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
 by (auto simp: union_of_def)
 then have "(arbitrary union_of P) (\C\\. \D\\. C \ D)"
 using R by (blast intro: arbitrary_union_of_Union)
 then show "(arbitrary union_of P) (S \ T)"
 by (simp add: Int_UN_distrib2 *)
qed
qed

lemma arbitrary_intersection_of_Un_eq:
 "(\S T. (arbitrary intersection_of P) S \ (arbitrary intersection_of P) T
 \<longrightarrow> (arbitrary intersection_of P) (S \<union> T)) \<longleftrightarrow>
 (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary intersection_of P) (S \<union> T))"
 apply (simp add: arbitrary_intersection_of_complement)
 using arbitrary_union_of_Int_eq [of "\S. P (- S)"]
 by (metis (no_types, lifting) arbitrary_def double_compl union_of_inc)

lemma finite_union_of_empty [simp]: "(finite union_of P) {}"
 by (simp add: union_of_empty)

lemma finite_intersection_of_empty [simp]: "(finite intersection_of P) UNIV"
 by (simp add: intersection_of_empty)

lemma finite_union_of_inc:
 "P S \ (finite union_of P) S"
 by (simp add: union_of_inc)

lemma finite_intersection_of_inc:
 "P S \ (finite intersection_of P) S"
 by (simp add: intersection_of_inc)

lemma finite_union_of_complement:
 "(finite union_of P) S \ (finite intersection_of (\S. P(- S))) (- S)"
 unfolding union_of_def intersection_of_def
 apply safe
 apply (rule_tac x="uminus ` \" in exI, fastforce)+
 done

lemma finite_intersection_of_complement:
 "(finite intersection_of P) S \ (finite union_of (\S. P(- S))) (- S)"
 by (simp add: finite_union_of_complement)

lemma finite_union_of_idempot [simp]:
 "finite union_of finite union_of P = finite union_of P"
proof -
 have "(finite union_of P) S" if S: "(finite union_of finite union_of P) S" for S
 proof -
 obtain \ where "finite \" "S = \<Union>\" and \: "\<forall>U\<in>\. \<exists>\. finite \ \<and> (\ \<subseteq> Collect P) \<and> \<Union>\ = U"
 using S unfolding union_of_def by (auto simp: subset_eq)
 then obtain f where "\U\\. finite (f U) \ (f U \ Collect P) \ \(f U) = U"
 by metis
 then show ?thesis
 unfolding union_of_def \<open>S = \<Union>\\<close>
 by (rule_tac x = "snd ` Sigma \ f" in exI) (fastforce simp: \finite \\)
 qed
 moreover
 have "(finite union_of finite union_of P) S" if "(finite union_of P) S" for S
 by (simp add: finite_union_of_inc that)
 ultimately show ?thesis
 by force
qed

lemma finite_intersection_of_idempot [simp]:
 "finite intersection_of finite intersection_of P = finite intersection_of P"
 by (force simp: finite_intersection_of_complement)

lemma finite_union_of_Union:
 "\finite \; \S. S \ \ \ (finite union_of P) S\ \ (finite union_of P) (\\)"
 using finite_union_of_idempot [of P]
 by (metis mem_Collect_eq subsetI union_of_def)

lemma finite_union_of_Un:
 "\(finite union_of P) S; (finite union_of P) T\ \ (finite union_of P) (S \ T)"
 by (auto simp: union_of_def)

lemma finite_intersection_of_Inter:
 "\finite \; \S. S \ \ \ (finite intersection_of P) S\ \ (finite intersection_of P) (\\)"
 using finite_intersection_of_idempot [of P]
 by (metis intersection_of_def mem_Collect_eq subsetI)

lemma finite_intersection_of_Int:
 "\(finite intersection_of P) S; (finite intersection_of P) T\
 \<Longrightarrow> (finite intersection_of P) (S \<inter> T)"
 by (auto simp: intersection_of_def)

lemma finite_union_of_Int_eq:
 "(\S T. (finite union_of P) S \ (finite union_of P) T \ (finite union_of P) (S \ T))
 \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (finite union_of P) (S \<inter> T))"
(is "?lhs = ?rhs")
proof
 assume ?lhs
 then show ?rhs
 by (simp add: finite_union_of_inc)
next
 assume R: ?rhs
 show ?lhs
 proof clarify
 fix S :: "'a set" and T :: "'a set"
 assume "(finite union_of P) S" and "(finite union_of P) T"
 then obtain \ \<V> where *: "\ \<subseteq> Collect P" "\<Union>\ = S" "finite \" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T" "finite \<V>"
 by (auto simp: union_of_def)
 then have "(finite union_of P) (\C\\. \D\\. C \ D)"
 using R
 by (blast intro: finite_union_of_Union)
 then show "(finite union_of P) (S \ T)"
 by (simp add: Int_UN_distrib2 *)
qed
qed

lemma finite_intersection_of_Un_eq:
 "(\S T. (finite intersection_of P) S \
 (finite intersection_of P) T
 \<longrightarrow> (finite intersection_of P) (S \<union> T)) \<longleftrightarrow>
 (\<forall>S T. P S \<and> P T \<longrightarrow> (finite intersection_of P) (S \<union> T))"
 apply (simp add: finite_intersection_of_complement)
 using finite_union_of_Int_eq [of "\S. P (- S)"]
 by (metis (no_types, lifting) double_compl)

abbreviation finite' :: "'a set \<Rightarrow> bool"
 where "finite' A \ finite A \ A \ {}"

lemma finite'_intersection_of_Int:
 "\(finite' intersection_of P) S; (finite' intersection_of P) T\
 \<Longrightarrow> (finite' intersection_of P) (S \<inter> T)"
 by (auto simp: intersection_of_def)

lemma finite'_intersection_of_inc:
 "P S \ (finite' intersection_of P) S"
 by (simp add: intersection_of_inc)

subsection \<open>The ``Relative to'' operator\<close>

text\<open>A somewhat cheap but handy way of getting localized forms of various topological concepts
(open, closed, borel, fsigma, gdelta etc.)\<close>

definition relative_to :: "['a set \ bool, 'a set, 'a set] \ bool" (infixl "relative'_to" 55)
 where "P relative_to S \ \T. \U. P U \ S \ U = T"

lemma relative_to_UNIV [simp]: "(P relative_to UNIV) S \ P S"
 by (simp add: relative_to_def)

lemma relative_to_imp_subset:
 "(P relative_to S) T \ T \ S"
 by (auto simp: relative_to_def)

lemma all_relative_to: "(\S. (P relative_to U) S \ Q S) \ (\S. P S \ Q(U \ S))"
 by (auto simp: relative_to_def)

lemma relative_toE: "\(P relative_to U) S; \S. P S \ Q(U \ S)\ \ Q S"
 by (auto simp: relative_to_def)

lemma relative_to_inc:
 "P S \ (P relative_to U) (U \ S)"
 by (auto simp: relative_to_def)

lemma relative_to_relative_to [simp]:
 "P relative_to S relative_to T = P relative_to (S \ T)"
 unfolding relative_to_def
 by auto

lemma relative_to_compl:
 "S \ U \ ((P relative_to U) (U - S) \ ((\c. P(- c)) relative_to U) S)"
 unfolding relative_to_def
 by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)

lemma relative_to_subset:
 "S \ T \ P S \ (P relative_to T) S"
 unfolding relative_to_def by auto

lemma relative_to_subset_trans:
 "(P relative_to U) S \ S \ T \ T \ U \ (P relative_to T) S"
 unfolding relative_to_def by auto

lemma relative_to_mono:
 "\(P relative_to U) S; \S. P S \ Q S\ \ (Q relative_to U) S"
 unfolding relative_to_def by auto

lemma relative_to_subset_inc: "\S \ U; P S\ \ (P relative_to U) S"
 unfolding relative_to_def by auto

lemma relative_to_Int:
 "\(P relative_to S) C; (P relative_to S) D; \X Y. \P X; P Y\ \ P(X \ Y)\
 \<Longrightarrow> (P relative_to S) (C \<inter> D)"
 unfolding relative_to_def by auto

lemma relative_to_Un:
 "\(P relative_to S) C; (P relative_to S) D; \X Y. \P X; P Y\ \ P(X \ Y)\
 \<Longrightarrow> (P relative_to S) (C \<union> D)"
 unfolding relative_to_def by auto

lemma arbitrary_union_of_relative_to:
 "((arbitrary union_of P) relative_to U) = (arbitrary union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Union>\" "\ \<subseteq> Collect P"
 using L unfolding relative_to_def union_of_def by auto
 then show ?thesis
 unfolding relative_to_def union_of_def arbitrary_def
 by (rule_tac x="(\X. U \ X) ` \" in exI) auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T"
 using R unfolding relative_to_def union_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "\\'\Collect P. \\' = \ (f ` \)"
 by (metis image_subset_iff mem_Collect_eq)
 moreover have eq: "U \ \ (f ` \) = \\"
 using f by auto
 ultimately show ?thesis
 unfolding relative_to_def union_of_def arbitrary_def \<open>S = \<Union>\\<close>
 by metis
 qed
 ultimately show ?thesis
 by blast
qed

lemma finite_union_of_relative_to:
 "((finite union_of P) relative_to U) = (finite union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Union>\" "\ \<subseteq> Collect P" "finite \"
 using L unfolding relative_to_def union_of_def by auto
 then show ?thesis
 unfolding relative_to_def union_of_def
 by (rule_tac x="(\X. U \ X) ` \" in exI) auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T" "finite \"
 using R unfolding relative_to_def union_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "\\'\Collect P. \\' = \ (f ` \)"
 by (metis image_subset_iff mem_Collect_eq)
 moreover have eq: "U \ \ (f ` \) = \\"
 using f by auto
 ultimately show ?thesis
 using \<open>finite \\<close> f
 unfolding relative_to_def union_of_def \<open>S = \<Union>\\<close>
 by (rule_tac x="\ (f ` \)" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
 qed
 ultimately show ?thesis
 by blast
qed

lemma countable_union_of_relative_to:
 "((countable union_of P) relative_to U) = (countable union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Union>\" "\ \<subseteq> Collect P" "countable \"
 using L unfolding relative_to_def union_of_def by auto
 then show ?thesis
 unfolding relative_to_def union_of_def
 by (rule_tac x="(\X. U \ X) ` \" in exI) auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T" "countable \"
 using R unfolding relative_to_def union_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "\\'\Collect P. \\' = \ (f ` \)"
 by (metis image_subset_iff mem_Collect_eq)
 moreover have eq: "U \ \ (f ` \) = \\"
 using f by auto
 ultimately show ?thesis
 using \<open>countable \\<close> f
 unfolding relative_to_def union_of_def \<open>S = \<Union>\\<close>
 by (rule_tac x="\ (f ` \)" in exI) (metis countable_image image_subsetI mem_Collect_eq)
 qed
 ultimately show ?thesis
 by blast
qed

lemma arbitrary_intersection_of_relative_to:
 "((arbitrary intersection_of P) relative_to U) = ((arbitrary intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where \: "S = U \<inter> \<Inter>\" "\ \<subseteq> Collect P"
 using L unfolding relative_to_def intersection_of_def by auto
 show ?thesis
 unfolding relative_to_def intersection_of_def arbitrary_def
 proof (intro exI conjI)
 show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}"
 using \ by blast+
 qed auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T"
 using R unfolding relative_to_def intersection_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "f ` \ \ Collect P"
 by auto
 moreover have eq: "U \ \(f ` \) = U \ \\"
 using f by auto
 ultimately show ?thesis
 unfolding relative_to_def intersection_of_def arbitrary_def \<open>S = U \<inter> \<Inter>\\<close>
 by auto
 qed
 ultimately show ?thesis
 by blast
qed

lemma finite_intersection_of_relative_to:
 "((finite intersection_of P) relative_to U) = ((finite intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where \: "S = U \<inter> \<Inter>\" "\ \<subseteq> Collect P" "finite \"
 using L unfolding relative_to_def intersection_of_def by auto
 show ?thesis
 unfolding relative_to_def intersection_of_def
 proof (intro exI conjI)
 show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}"
 using \ by blast+
 show "finite ((\) U ` \)"
 by (simp add: \<open>finite \\<close>)
 qed auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T" "finite \"
 using R unfolding relative_to_def intersection_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "f ` \ \ Collect P"
 by auto
 moreover have eq: "U \ \ (f ` \) = U \ \ \"
 using f by auto
 ultimately show ?thesis
 unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\\<close>
 using \<open>finite \\<close>
 by auto
 qed
 ultimately show ?thesis
 by blast
qed

lemma countable_intersection_of_relative_to:
 "((countable intersection_of P) relative_to U) = ((countable intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
 have "?rhs S" if L: "?lhs S" for S
 proof -
 obtain \ where \: "S = U \<inter> \<Inter>\" "\ \<subseteq> Collect P" "countable \"
 using L unfolding relative_to_def intersection_of_def by auto
 show ?thesis
 unfolding relative_to_def intersection_of_def
 proof (intro exI conjI)
 show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}"
 using \ by blast+
 show "countable ((\) U ` \)"
 by (simp add: \<open>countable \\<close>)
 qed auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> V = T" "countable \"
 using R unfolding relative_to_def intersection_of_def by auto
 then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T"
 by metis
 then have "f ` \ \ Collect P"
 by auto
 moreover have eq: "U \ \ (f ` \) = U \ \ \"
 using f by auto
 ultimately show ?thesis
 unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\\<close>
 using \<open>countable \\<close> countable_image
 by auto
 qed
 ultimately show ?thesis
 by blast
qed

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.