Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Poly_Mapping.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.47 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Poly_Mapping.thy Sprache: Isabelle

Original von: Isabelle^©

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Laden

in der Quellcodebibliothek suchen

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Poly_Mapping.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Laden

in der Quellcodebibliothek suchen

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©