Quelle Equipollence.thy Sprache: Isabelle

section \<open>Equipollence and Other Relations Connected with Cardinality\<close>

theory "Equipollence"
  imports FuncSet Countable_Set
begin

subsection\<open>Eqpoll\<close>

definition eqpoll :: "'a set \ 'b set \ bool" (infixl \\\ 50)
  where "eqpoll A B \ \f. bij_betw f A B"

definition lepoll :: "'a set \ 'b set \ bool" (infixl \\\ 50)
  where "lepoll A B \ \f. inj_on f A \ f ` A \ B"

definition lesspoll :: "'a set \ 'b set \ bool" (infixl \\\ 50)
  where "A \ B == A \ B \ ~(A \ B)"

lemma lepoll_def': "lepoll A B \ \f. inj_on f A \ f \ A \ B"
  by (simp add: Pi_iff image_subset_iff lepoll_def)

lemma eqpoll_empty_iff_empty [simp]: "A \ {} \ A={}"
  by (simp add: bij_betw_iff_bijections eqpoll_def)

lemma lepoll_empty_iff_empty [simp]: "A \ {} \ A = {}"
  by (auto simp: lepoll_def)

lemma not_lesspoll_empty: "\ A \ {}"
  by (simp add: lesspoll_def)

(*The HOL Light CARD_LE_RELATIONAL_FULL*)
lemma lepoll_relational_full:
  assumes "\y. y \ B \ \x. x \ A \ R x y"
    and "\x y y'. \x \ A; y \ B; y' \ B; R x y; R x y'\ \ y = y'"
  shows "B \ A"
proof -
  obtain f where f: "\y. y \ B \ f y \ A \ R (f y) y"
    using assms by metis
  with assms have "inj_on f B"
    by (metis inj_onI)
  with f show ?thesis
    unfolding lepoll_def by blast
qed

lemma eqpoll_iff_card_of_ordIso: "A \ B \ ordIso2 (card_of A) (card_of B)"
  by (simp add: card_of_ordIso eqpoll_def)

lemma eqpoll_refl [iff]: "A \ A"
  by (simp add: card_of_refl eqpoll_iff_card_of_ordIso)

lemma eqpoll_finite_iff: "A \ B \ finite A \ finite B"
  by (meson bij_betw_finite eqpoll_def)

lemma eqpoll_iff_card:
  assumes "finite A" "finite B"
  shows  "A \ B \ card A = card B"
  using assms by (auto simp: bij_betw_iff_card eqpoll_def)

lemma eqpoll_singleton_iff: "A \ {x} \ (\u. A = {u})"
  by (metis card.infinite card_1_singleton_iff eqpoll_finite_iff eqpoll_iff_card not_less_eq_eq)

lemma eqpoll_doubleton_iff: "A \ {x,y} \ (\u v. A = {u,v} \ (u=v \ x=y))"
proof (cases "x=y")
  case True
  then show ?thesis
    by (simp add: eqpoll_singleton_iff)
next
  case False
  then show ?thesis
    by (smt (verit, ccfv_threshold) card_1_singleton_iff card_Suc_eq_finite eqpoll_finite_iff
        eqpoll_iff_card finite.insertI singleton_iff)
qed

lemma lepoll_antisym:
  assumes "A \ B" "B \ A" shows "A \ B"
  using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)

lemma lepoll_trans [trans]:
  assumes "A \ B" " B \ C" shows "A \ C"
proof -
  obtain f g where fg: "inj_on f A" "inj_on g B" and "f : A \ B" "g \ B \ C"
    by (metis assms lepoll_def')
  then have "g \ f \ A \ C"
    by auto
  with fg show ?thesis
    unfolding lepoll_def
    by (metis \<open>f \<in> A \<rightarrow> B\<close> comp_inj_on image_subset_iff_funcset inj_on_subset)
qed

lemma lepoll_trans1 [trans]: "\A \ B; B \ C\ \ A \ C"
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)

lemma lepoll_trans2 [trans]: "\A \ B; B \ C\ \ A \ C"
  by (metis bij_betw_def eqpoll_def lepoll_def lepoll_trans order_refl)

lemma eqpoll_sym: "A \ B \ B \ A"
  unfolding eqpoll_def
  using bij_betw_the_inv_into by auto

lemma eqpoll_trans [trans]: "\A \ B; B \ C\ \ A \ C"
  unfolding eqpoll_def using bij_betw_trans by blast

lemma eqpoll_imp_lepoll: "A \ B \ A \ B"
  unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)

lemma subset_imp_lepoll: "A \ B \ A \ B"
  by (force simp: lepoll_def)

lemma lepoll_refl [iff]: "A \ A"
  by (simp add: subset_imp_lepoll)

lemma lepoll_iff: "A \ B \ (\g. A \ g ` B)"
  unfolding lepoll_def
proof safe
  fix g assume "A \ g ` B"
  then show "\f. inj_on f A \ f ` A \ B"
    by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
qed (metis image_mono the_inv_into_onto)

lemma empty_lepoll [iff]: "{} \ A"
  by (simp add: lepoll_iff)

lemma subset_image_lepoll: "B \ f ` A \ B \ A"
  by (auto simp: lepoll_iff)

lemma image_lepoll: "f ` A \ A"
  by (auto simp: lepoll_iff)

lemma infinite_le_lepoll: "infinite A \ (UNIV::nat set) \ A"
  by (simp add: infinite_iff_countable_subset lepoll_def)

lemma lepoll_Pow_self: "A \ Pow A"
  unfolding lepoll_def inj_def
  proof (intro exI conjI)
    show "inj_on (\x. {x}) A"
      by (auto simp: inj_on_def)
qed auto

lemma eqpoll_iff_bijections:
   "A \ B \ (\f g. (\x \ A. f x \ B \ g(f x) = x) \ (\y \ B. g y \ A \ f(g y) = y))"
    by (auto simp: eqpoll_def bij_betw_iff_bijections)

lemma lepoll_restricted_funspace:
   "{f. f ` A \ B \ {x. f x \ k x} \ A \ finite {x. f x \ k x}} \ Fpow (A \ B)"
proof -
  have *: "\U \ Fpow (A \ B). f = (\x. if \y. (x, y) \ U then SOME y. (x,y) \ U else k x)"
    if "f ` A \ B" "{x. f x \ k x} \ A" "finite {x. f x \ k x}" for f
    apply (rule_tac x="(\x. (x, f x)) ` {x. f x \ k x}" in bexI)
    using that by (auto simp: image_def Fpow_def)
  show ?thesis
    apply (rule subset_image_lepoll [where f = "\U x. if \y. (x,y) \ U then @y. (x,y) \ U else k x"])
    using * by (auto simp: image_def)
qed

lemma singleton_lepoll: "{x} \ insert y A"
  by (force simp: lepoll_def)

lemma singleton_eqpoll: "{x} \ {y}"
  by (blast intro: lepoll_antisym singleton_lepoll)

lemma subset_singleton_iff_lepoll: "(\x. S \ {x}) \ S \ {()}"
  using lepoll_iff by fastforce

lemma infinite_insert_lepoll:
  assumes "infinite A" shows "insert a A \ A"
proof -
  obtain f :: "nat \ 'a" where "inj f" and f: "range f \ A"
    using assms infinite_countable_subset by blast
  let ?g = "(\z. if z=a then f 0 else if z \ range f then f (Suc (inv f z)) else z)"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?g (insert a A)"
      using inj_on_eq_iff [OF \<open>inj f\<close>]
      by (auto simp: inj_on_def)
    show "?g ` insert a A \ A"
      using f by auto
  qed
qed

lemma infinite_insert_eqpoll: "infinite A \ insert a A \ A"
  by (simp add: lepoll_antisym infinite_insert_lepoll subset_imp_lepoll subset_insertI)

lemma finite_lepoll_infinite:
  assumes "infinite A" "finite B" shows "B \ A"
proof -
  have "B \ (UNIV::nat set)"
    unfolding lepoll_def
    using finite_imp_inj_to_nat_seg [OF \<open>finite B\<close>] by blast
  then show ?thesis
    using \<open>infinite A\<close> infinite_le_lepoll lepoll_trans by auto
qed

lemma countable_lepoll: "\countable A; B \ A\ \ countable B"
  by (meson countable_image countable_subset lepoll_iff)

lemma countable_eqpoll: "\countable A; B \ A\ \ countable B"
  using countable_lepoll eqpoll_imp_lepoll by blast

subsection\<open>The strict relation\<close>

lemma lesspoll_not_refl [iff]: "~ (i \ i)"
  by (simp add: lepoll_antisym lesspoll_def)

lemma lesspoll_imp_lepoll: "A \ B ==> A \ B"
by (unfold lesspoll_def, blast)

lemma lepoll_iff_leqpoll: "A \ B \ A \ B | A \ B"
  using eqpoll_imp_lepoll lesspoll_def by blast

lemma lesspoll_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans1 [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)

lemma lesspoll_trans2 [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)

lemma eq_lesspoll_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  using eqpoll_imp_lepoll lesspoll_trans1 by blast

lemma lesspoll_eq_trans [trans]: "\X \ Y; Y \ Z\ \ X \ Z"
  using eqpoll_imp_lepoll lesspoll_trans2 by blast

lemma lesspoll_Pow_self: "A \ Pow A"
  unfolding lesspoll_def bij_betw_def eqpoll_def
  by (meson lepoll_Pow_self Cantors_theorem)

lemma finite_lesspoll_infinite:
  assumes "infinite A" "finite B" shows "B \ A"
  by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def)

lemma countable_lesspoll: "\countable A; B \ A\ \ countable B"
  using countable_lepoll lesspoll_def by blast

lemma lepoll_iff_card_le: "\finite A; finite B\ \ A \ B \ card A \ card B"
  by (simp add: inj_on_iff_card_le lepoll_def)

lemma lepoll_iff_finite_card: "A \ {.. finite A \ card A \ n"
  by (metis card_lessThan finite_lessThan finite_surj lepoll_iff lepoll_iff_card_le)

lemma eqpoll_iff_finite_card: "A \ {.. finite A \ card A = n"
  by (metis card_lessThan eqpoll_finite_iff eqpoll_iff_card finite_lessThan)

lemma lesspoll_iff_finite_card: "A \ {.. finite A \ card A < n"
  by (metis eqpoll_iff_finite_card lepoll_iff_finite_card lesspoll_def order_less_le)

subsection\<open>Mapping by an injection\<close>

lemma inj_on_image_eqpoll_self: "inj_on f A \ f ` A \ A"
  by (meson bij_betw_def eqpoll_def eqpoll_sym)

lemma inj_on_image_lepoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (meson assms image_lepoll lepoll_def lepoll_trans order_refl)

lemma inj_on_image_lepoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (meson assms eq_iff image_lepoll lepoll_def lepoll_trans)

lemma inj_on_image_lesspoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (meson assms image_lepoll le_less lepoll_def lesspoll_trans1)

lemma inj_on_image_lesspoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (meson assms eqpoll_sym inj_on_image_eqpoll_self lesspoll_eq_trans)

lemma inj_on_image_eqpoll_1 [simp]:
  assumes "inj_on f A" shows "f ` A \ B \ A \ B"
  by (metis assms eqpoll_trans inj_on_image_eqpoll_self eqpoll_sym)

lemma inj_on_image_eqpoll_2 [simp]:
  assumes "inj_on f B" shows "A \ f ` B \ A \ B"
  by (metis assms inj_on_image_eqpoll_1 eqpoll_sym)

subsection \<open>Inserting elements into sets\<close>

lemma insert_lepoll_insertD:
  assumes "insert u A \ insert v B" "u \ A" "v \ B" shows "A \ B"
proof -
  obtain f where inj: "inj_on f (insert u A)" and fim: "f ` (insert u A) \ insert v B"
    by (meson assms lepoll_def)
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?g = "\x\A. if f x = v then f u else f x"
    show "inj_on ?g A"
      using inj \<open>u \<notin> A\<close> by (auto simp: inj_on_def)
    show "?g ` A \ B"
      using fim \<open>u \<notin> A\<close> image_subset_iff inj inj_on_image_mem_iff by fastforce
  qed
qed

lemma insert_eqpoll_insertD: "\insert u A \ insert v B; u \ A; v \ B\ \ A \ B"
  by (meson insert_lepoll_insertD eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma insert_lepoll_cong:
  assumes "A \ B" "b \ B" shows "insert a A \ insert b B"
proof -
  obtain f where f: "inj_on f A" "f ` A \ B"
    by (meson assms lepoll_def)
  let ?f = "\u \ insert a A. if u=a then b else f u"
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ?f (insert a A)"
      using f \<open>b \<notin> B\<close> by (auto simp: inj_on_def)
    show "?f ` insert a A \ insert b B"
      using f \<open>b \<notin> B\<close> by auto
  qed
qed

lemma insert_eqpoll_cong:
     "\A \ B; a \ A; b \ B\ \ insert a A \ insert b B"
  by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong lepoll_antisym)

lemma insert_eqpoll_insert_iff:
     "\a \ A; b \ B\ \ insert a A \ insert b B \ A \ B"
  by (meson insert_eqpoll_insertD insert_eqpoll_cong)

lemma insert_lepoll_insert_iff:
     " \a \ A; b \ B\ \ (insert a A \ insert b B) \ (A \ B)"
  by (meson insert_lepoll_insertD insert_lepoll_cong)

lemma less_imp_insert_lepoll:
  assumes "A \ B" shows "insert a A \ B"
proof -
  obtain f where "inj_on f A" "f ` A \ B"
    using assms by (metis bij_betw_def eqpoll_def lepoll_def lesspoll_def psubset_eq)
  then obtain b where b: "b \ B" "b \ f ` A"
    by auto
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on (f(a:=b)) (insert a A)"
      using b \<open>inj_on f A\<close> by (auto simp: inj_on_def)
    show "(f(a:=b)) ` insert a A \ B"
      using \<open>f ` A \<subset> B\<close>  by (auto simp: b)
  qed
qed

lemma finite_insert_lepoll: "finite A \ (insert a A \ A) \ (a \ A)"
proof (induction A rule: finite_induct)
  case (insert x A)
  then show ?case
    by (metis insertI2 insert_lepoll_insert_iff insert_subsetI lepoll_trans subsetI subset_imp_lepoll)
qed auto

subsection\<open>Binary sums and unions\<close>

lemma Un_lepoll_mono:
  assumes "A \ C" "B \ D" "disjnt C D" shows "A \ B \ C \ D"
proof -
  obtain f g where inj: "inj_on f A" "inj_on g B" and fg: "f ` A \ C" "g ` B \ D"
    by (meson assms lepoll_def)
  have "inj_on (\x. if x \ A then f x else g x) (A \ B)"
    using inj \<open>disjnt C D\<close> fg unfolding disjnt_iff
    by (fastforce intro: inj_onI dest: inj_on_contraD split: if_split_asm)
  with fg show ?thesis
    unfolding lepoll_def
    by (rule_tac x="\x. if x \ A then f x else g x" in exI) auto
qed

lemma Un_eqpoll_cong: "\A \ C; B \ D; disjnt A B; disjnt C D\ \ A \ B \ C \ D"
  by (meson Un_lepoll_mono eqpoll_imp_lepoll eqpoll_sym lepoll_antisym)

lemma sum_lepoll_mono:
  assumes "A \ C" "B \ D" shows "A <+> B \ C <+> D"
proof -
  obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="case_sum (Inl \ f) (Inr \ g)" in exI) (force simp: inj_on_def)
qed

lemma sum_eqpoll_cong: "\A \ C; B \ D\ \ A <+> B \ C <+> D"
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym sum_lepoll_mono)

subsection\<open>Binary Cartesian products\<close>

lemma times_square_lepoll: "A \ A \ A"
  unfolding lepoll_def inj_def
proof (intro exI conjI)
  show "inj_on (\x. (x,x)) A"
    by (auto simp: inj_on_def)
qed auto

lemma times_commute_eqpoll: "A \ B \ B \ A"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "\(x,y). (y,x)" and f' = "\(x,y). (y,x)"])

lemma times_assoc_eqpoll: "(A \ B) \ C \ A \ (B \ C)"
  unfolding eqpoll_def
  by (force intro: bij_betw_byWitness [where f = "\((x,y),z). (x,(y,z))" and f' = "\(x,(y,z)). ((x,y),z)"])

lemma times_singleton_eqpoll: "{a} \ A \ A"
proof -
  have "{a} \ A = (\x. (a,x)) ` A"
    by auto
  also have "\ \ A"
    proof (rule inj_on_image_eqpoll_self)
      show "inj_on (Pair a) A"
        by (auto simp: inj_on_def)
    qed
    finally show ?thesis .
qed

lemma times_lepoll_mono:
  assumes "A \ C" "B \ D" shows "A \ B \ C \ D"
proof -
  obtain f g where "inj_on f A" "f ` A \ C" "inj_on g B" "g ` B \ D"
    by (meson assms lepoll_def)
  then show ?thesis
    unfolding lepoll_def
    by (rule_tac x="\(x,y). (f x, g y)" in exI) (auto simp: inj_on_def)
qed

lemma times_eqpoll_cong: "\A \ C; B \ D\ \ A \ B \ C \ D"
  by (metis eqpoll_imp_lepoll eqpoll_sym lepoll_antisym times_lepoll_mono)

lemma
  assumes "B \ {}" shows lepoll_times1: "A \ A \ B" and lepoll_times2: "A \ B \ A"
  using assms lepoll_iff by fastforce+

lemma times_0_eqpoll: "{} \ A \ {}"
  by (simp add: eqpoll_iff_bijections)

lemma Sigma_inj_lepoll_mono:
  assumes h: "inj_on h A" "h ` A \ C" and "\x. x \ A \ B x \ D (h x)"
  shows "Sigma A B \ Sigma C D"
proof -
  have "\x. x \ A \ \f. inj_on f (B x) \ f ` (B x) \ D (h x)"
    by (meson assms lepoll_def)
  then obtain f where  "\x. x \ A \ inj_on (f x) (B x) \ f x ` B x \ D (h x)"
    by metis
  with h show ?thesis
    unfolding lepoll_def inj_on_def
    by (rule_tac x="\(x,y). (h x, f x y)" in exI) force
qed

lemma Sigma_lepoll_mono:
  assumes "A \ C" "\x. x \ A \ B x \ D x" shows "Sigma A B \ Sigma C D"
  using Sigma_inj_lepoll_mono [of id] assms by auto

lemma sum_times_distrib_eqpoll: "(A <+> B) \ C \ (A \ C) <+> (B \ C)"
  unfolding eqpoll_def
proof
  show "bij_betw (\(x,z). case_sum(\y. Inl(y,z)) (\y. Inr(y,z)) x) ((A <+> B) \ C) (A \ C <+> B \ C)"
    by (rule bij_betw_byWitness [where f' = "case_sum (\(x,z). (Inl x, z)) (\(y,z). (Inr y, z))"]) auto
qed

lemma Sigma_eqpoll_cong:
  assumes h: "bij_betw h A C"  and BD: "\x. x \ A \ B x \ D (h x)"
  shows "Sigma A B \ Sigma C D"
proof (intro lepoll_antisym)
  show "Sigma A B \ Sigma C D"
    by (metis Sigma_inj_lepoll_mono bij_betw_def eqpoll_imp_lepoll subset_refl assms)
  have "inj_on (inv_into A h) C \ inv_into A h ` C \ A"
    by (metis bij_betw_def bij_betw_inv_into h set_eq_subset)
  then show "Sigma C D \ Sigma A B"
    by (smt (verit, best) BD Sigma_inj_lepoll_mono bij_betw_inv_into_right eqpoll_sym h image_subset_iff lepoll_refl lepoll_trans2)
qed

lemma prod_insert_eqpoll:
  assumes "a \ A" shows "insert a A \ B \ B <+> A \ B"
  unfolding eqpoll_def
  proof
  show "bij_betw (\(x,y). if x=a then Inl y else Inr (x,y)) (insert a A \ B) (B <+> A \ B)"
    by (rule bij_betw_byWitness [where f' = "case_sum (\y. (a,y)) id"]) (auto simp: assms)
qed

subsection\<open>General Unions\<close>

lemma Union_eqpoll_Times:
  assumes B: "\x. x \ A \ F x \ B" and disj: "pairwise (\x y. disjnt (F x) (F y)) A"
  shows "(\x\A. F x) \ A \ B"
proof (rule lepoll_antisym)
  obtain b where b: "\x. x \ A \ bij_betw (b x) (F x) B"
    using B unfolding eqpoll_def by metis
  show "\(F ` A) \ A \ B"
    unfolding lepoll_def
  proof (intro exI conjI)
    define \<chi> where "\<chi> \<equiv> \<lambda>z. THE x. x \<in> A \<and> z \<in> F x"
    have \<chi>: "\<chi> z = x" if "x \<in> A" "z \<in> F x" for x z
      unfolding \<chi>_def
      by (smt (verit, best) disj disjnt_iff pairwiseD that(1,2) theI_unique)
    let ?f = "\z. (\ z, b (\ z) z)"
    show "inj_on ?f (\(F ` A))"
      unfolding inj_on_def
      by clarify (metis \<chi> b bij_betw_inv_into_left)
    show "?f ` \(F ` A) \ A \ B"
      using \<chi> b bij_betwE by blast
  qed
  show "A \ B \ \(F ` A)"
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?f = "\(x,y). inv_into (F x) (b x) y"
    have *: "inv_into (F x) (b x) y \ F x" if "x \ A" "y \ B" for x y
      by (metis b bij_betw_imp_surj_on inv_into_into that)
    then show "inj_on ?f (A \ B)"
      unfolding inj_on_def
      by clarsimp (metis (mono_tags, lifting) b bij_betw_inv_into_right disj disjnt_iff pairwiseD)
    show "?f ` (A \ B) \ \ (F ` A)"
      by clarsimp (metis b bij_betw_imp_surj_on inv_into_into)
  qed
qed

lemma UN_lepoll_UN:
  assumes A: "\x. x \ A \ B x \ C x"
    and disj: "pairwise (\x y. disjnt (C x) (C y)) A"
  shows "\ (B`A) \ \ (C`A)"
proof -
  obtain f where f: "\x. x \ A \ inj_on (f x) (B x) \ f x ` (B x) \ (C x)"
    using A unfolding lepoll_def by metis
  show ?thesis
    unfolding lepoll_def
  proof (intro exI conjI)
    define \<chi> where "\<chi> \<equiv> \<lambda>z. @x. x \<in> A \<and> z \<in> B x"
    have \<chi>: "\<chi> z \<in> A \<and> z \<in> B (\<chi> z)" if "x \<in> A" "z \<in> B x" for x z
      unfolding \<chi>_def by (metis (mono_tags, lifting) someI_ex that)
    let ?f = "\z. (f (\ z) z)"
    show "inj_on ?f (\(B ` A))"
      using disj f unfolding inj_on_def disjnt_iff pairwise_def image_subset_iff
      by (metis UN_iff \<chi>)
    show "?f ` \ (B ` A) \ \ (C ` A)"
      using \<chi> f unfolding image_subset_iff by blast
  qed
qed

lemma UN_eqpoll_UN:
  assumes A: "\x. x \ A \ B x \ C x"
    and B: "pairwise (\x y. disjnt (B x) (B y)) A"
    and C: "pairwise (\x y. disjnt (C x) (C y)) A"
  shows "(\x\A. B x) \ (\x\A. C x)"
proof (rule lepoll_antisym)
  show "\ (B ` A) \ \ (C ` A)"
    by (meson A C UN_lepoll_UN eqpoll_imp_lepoll)
  show "\ (C ` A) \ \ (B ` A)"
    by (simp add: A B UN_lepoll_UN eqpoll_imp_lepoll eqpoll_sym)
qed

subsection\<open>General Cartesian products (Pi)\<close>

lemma PiE_sing_eqpoll_self: "({a} \\<^sub>E B) \ B"
proof -
  have 1: "x = y"
    if "x \ {a} \\<^sub>E B" "y \ {a} \\<^sub>E B" "x a = y a" for x y
    by (metis IntD2 PiE_def extensionalityI singletonD that)
  have 2: "x \ (\h. h a) ` ({a} \\<^sub>E B)" if "x \ B" for x
    using that by (rule_tac x="\z\{a}. x" in image_eqI) auto
  show ?thesis
  unfolding eqpoll_def bij_betw_def inj_on_def
  by (force intro: 1 2)
qed

lemma lepoll_funcset_right:
  assumes "B \ B'" shows "A \\<^sub>E B \ A \\<^sub>E B'"
proof -
  obtain f where f: "inj_on f B" "f ` B \ B'"
    by (meson assms lepoll_def)
  let ?G = "\g. \z \ A. f(g z)"
  have "inj_on ?G (A \\<^sub>E B)"
    using f by (smt (verit, best) PiE_ext PiE_mem inj_on_def restrict_apply')
  moreover have "?G ` (A \\<^sub>E B) \ (A \\<^sub>E B')"
    using f by fastforce
  ultimately show ?thesis
    by (meson lepoll_def)
qed

lemma lepoll_funcset_left:
  assumes "B \ {}" "A \ A'"
  shows "A \\<^sub>E B \ A' \\<^sub>E B"
proof -
  obtain b where "b \ B"
    using assms by blast
  obtain f where "inj_on f A" and fim: "f ` A \ A'"
    using assms by (auto simp: lepoll_def)
  then obtain h where h: "\x. x \ A \ h (f x) = x"
    using the_inv_into_f_f by fastforce
  let ?F = "\g. \u \ A'. if h u \ A then g(h u) else b"
  show ?thesis
    unfolding lepoll_def inj_on_def
  proof (intro exI conjI ballI impI ext)
    fix k l x
    assume k: "k \ A \\<^sub>E B" and l: "l \ A \\<^sub>E B" and "?F k = ?F l"
    then have "?F k (f x) = ?F l (f x)"
      by simp
    then show "k x = l x"
      by (smt (verit, best) PiE_arb fim h image_subset_iff k l restrict_apply')
  next
    show "?F ` (A \\<^sub>E B) \ A' \\<^sub>E B"
      using \<open>b \<in> B\<close> by force
  qed
qed

lemma lepoll_funcset:
   "\B \ {}; A \ A'; B \ B'\ \ A \\<^sub>E B \ A' \\<^sub>E B'"
  by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto

lemma lepoll_PiE:
  assumes "\i. i \ A \ B i \ C i"
  shows "PiE A B \ PiE A C"
proof -
  obtain f where f: "\i. i \ A \ inj_on (f i) (B i) \ (f i) ` B i \ C i"
    using assms unfolding lepoll_def by metis
  let ?G = "\g. \i \ A. f i (g i)"
  have "inj_on ?G (PiE A B)"
    by (smt (verit, ccfv_SIG) PiE_ext PiE_iff f inj_on_def restrict_apply')
  moreover have "?G ` (PiE A B) \ (PiE A C)"
    using f by fastforce
  ultimately show ?thesis
    by (meson lepoll_def)
qed

lemma card_le_PiE_subindex:
  assumes "A \ A'" "Pi\<^sub>E A' B \ {}"
  shows "PiE A B \ PiE A' B"
proof -
  have "\x. x \ A' \ \y. y \ B x"
    using assms by blast
  then obtain g where g: "\x. x \ A' \ g x \ B x"
    by metis
  let ?F = "\f x. if x \ A then f x else if x \ A' then g x else undefined"
  have "Pi\<^sub>E A B \ (\f. restrict f A) ` Pi\<^sub>E A' B"
  proof
    show "f \ Pi\<^sub>E A B \ f \ (\f. restrict f A) ` Pi\<^sub>E A' B" for f
      using \<open>A \<subseteq> A'\<close>
      by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
  qed
  then have "Pi\<^sub>E A B \ (\f. \i \ A. f i) ` Pi\<^sub>E A' B"
    by (simp add: subset_imp_lepoll)
  also have "\ \ PiE A' B"
    by (rule image_lepoll)
  finally show ?thesis .
qed

lemma finite_restricted_funspace:
  assumes "finite A" "finite B"
  shows "finite {f. f ` A \ B \ {x. f x \ k x} \ A}" (is "finite ?F")
proof (rule finite_subset)
  show "finite ((\U x. if \y. (x,y) \ U then @y. (x,y) \ U else k x) ` Pow(A \ B))" (is "finite ?G")
    using assms by auto
  show "?F \ ?G"
  proof
    fix f
    assume "f \ ?F"
    then show "f \ ?G"
      by (rule_tac x="(\x. (x,f x)) ` {x. f x \ k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
  qed
qed

proposition finite_PiE_iff:
   "finite(PiE I S) \ PiE I S = {} \ finite {i \ I. ~(\a. S i \ {a})} \ (\i \ I. finite(S i))"
(is "?lhs = ?rhs")
proof (cases "PiE I S = {}")
  case False
  define J where "J \ {i \ I. \a. S i \ {a}}"
  show ?thesis
  proof
    assume L: ?lhs
    have "infinite (Pi\<^sub>E I S)" if "infinite J"
    proof -
      have "(UNIV::nat set) \ (UNIV::(nat\bool) set)"
      proof -
        have "\N::nat set. inj_on (=) N"
          by (simp add: inj_on_def)
        then show ?thesis
          by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
      qed
      also have "\ = (UNIV::nat set) \\<^sub>E (UNIV::bool set)"
        by auto
      also have "\ \ J \\<^sub>E (UNIV::bool set)"
        by (metis empty_not_UNIV infinite_le_lepoll lepoll_funcset_left that)
      also have "\ \ Pi\<^sub>E J S"
      proof -
        have *: "(UNIV::bool set) \ S i" if "i \ I" and \

: "\a. \ S i \ {a}" for i
        proof -
          obtain a b where "{a,b} \ S i" "a \ b"
            by (metis \<section> empty_subsetI insert_subset subsetI)
          then show ?thesis
            by (metis Set.set_insert UNIV_bool insert_iff insert_lepoll_cong insert_subset singleton_lepoll)
        qed
        show ?thesis
          by (auto simp: * J_def intro: lepoll_PiE)
      qed
      also have "\ \ Pi\<^sub>E I S"
        using False by (auto simp: J_def intro: card_le_PiE_subindex)
      finally have "(UNIV::nat set) \ Pi\<^sub>E I S" .
      then show ?thesis
        by (simp add: infinite_le_lepoll)
    qed
    moreover have "finite (S i)" if "i \ I" for i
    proof (rule finite_subset)
      obtain f where f: "f \ PiE I S"
        using False by blast
      show "S i \ (\f. f i) ` Pi\<^sub>E I S"
      proof
        show "s \ (\f. f i) ` Pi\<^sub>E I S" if "s \ S i" for s
          using that f \<open>i \<in> I\<close>
          by (rule_tac x="\j. if j = i then s else f j" in image_eqI) auto
      qed
    next
      show "finite ((\x. x i) ` Pi\<^sub>E I S)"
        using L by blast
    qed
    ultimately show ?rhs
      using L
      by (auto simp: J_def False)
  next
    assume R: ?rhs
    have "\i \ I - J. \a. S i = {a}"
      using False J_def by blast
    then obtain a where a: "\i \ I - J. S i = {a i}"
      by metis
    let ?F = "{f. f ` J \ (\i \ J. S i) \ {i. f i \ (if i \ I then a i else undefined)} \ J}"
    have *: "finite (Pi\<^sub>E I S)"
      if "finite J" and "\i\I. finite (S i)"
    proof (rule finite_subset)
      have "\f j. \f \ Pi\<^sub>E I S; j \ J\ \ f j \ \ (S ` J)"
        using J_def by blast
      moreover
      have "\f j. \f \ Pi\<^sub>E I S; f j \ (if j \ I then a j else undefined)\ \ j \ J"
        by (metis DiffI PiE_E a singletonD)
      ultimately show "Pi\<^sub>E I S \ ?F" by force
      show "finite ?F"
      proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
        show "finite (\ (S ` J))"
          using that J_def by blast
      qed
  qed
  show ?lhs
      using R by (auto simp: * J_def)
  qed
qed auto

corollary finite_funcset_iff:
  "finite(I \\<^sub>E S) \ (\a. S \ {a}) \ I = {} \ finite I \ finite S"
  by (fastforce simp: finite_PiE_iff PiE_eq_empty_iff dest: subset_singletonD)

subsection \<open>Misc other resultd\<close>

lemma lists_lepoll_mono:
  assumes "A \ B" shows "lists A \ lists B"
proof -
  obtain f where f: "inj_on f A" "f ` A \ B"
    by (meson assms lepoll_def)
  moreover have "inj_on (map f) (lists A)"
    using f unfolding inj_on_def
    by clarsimp (metis list.inj_map_strong)
  ultimately show ?thesis
    unfolding lepoll_def by force
qed

lemma lepoll_lists: "A \ lists A"
  unfolding lepoll_def inj_on_def by(rule_tac x="\x. [x]" in exI) auto

text \<open>Dedekind's definition of infinite set\<close>

lemma infinite_iff_psubset: "infinite A \ (\B. B \ A \ A\B)"
proof
  assume "infinite A"
  then obtain f :: "nat \ 'a" where "inj f" and f: "range f \ A"
    by (meson infinite_countable_subset)
  define C where "C \ A - range f"
  have C: "A = range f \ C" "range f \ C = {}"
    using f by (auto simp: C_def)
  have *: "range (f \ Suc) \ range f"
    using inj_eq [OF \<open>inj f\<close>] by (fastforce simp: set_eq_iff)
  have "range f \ C \ range (f \ Suc) \ C"
  proof (intro Un_eqpoll_cong)
    show "range f \ range (f \ Suc)"
      by (meson \<open>inj f\<close> eqpoll_refl inj_Suc inj_compose inj_on_image_eqpoll_2)
    show "disjnt (range f) C"
      by (simp add: C disjnt_def)
    then show "disjnt (range (f \ Suc)) C"
      using "*" disjnt_subset1 by blast
  qed auto
  moreover have "range (f \ Suc) \ C \ A"
    using "*" f C_def by blast
  ultimately show "\B\A. A \ B"
    by (metis C(1))
next
  assume "\B\A. A \ B" then show "infinite A"
    by (metis card_subset_eq eqpoll_finite_iff eqpoll_iff_card psubsetE)
qed

lemma infinite_iff_psubset_le: "infinite A \ (\B. B \ A \ A \ B)"
  by (meson eqpoll_imp_lepoll infinite_iff_psubset lepoll_antisym psubsetE subset_imp_lepoll)

end

quality100%

¤ 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.0.17Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.