src/HOL/Library/Equipollence.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69874 11065b70407d
permissions -rw-r--r--
improved code equations taken over from AFP
lp15@69735
     1
section \<open>Equipollence and Other Relations Connected with Cardinality\<close>
lp15@69735
     2
lp15@69735
     3
theory "Equipollence"
lp15@69735
     4
  imports FuncSet
lp15@69735
     5
begin
lp15@69735
     6
lp15@69735
     7
subsection\<open>Eqpoll\<close>
lp15@69735
     8
lp15@69735
     9
definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<approx>" 50)
lp15@69735
    10
  where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B"
lp15@69735
    11
lp15@69735
    12
definition lepoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<lesssim>" 50)
lp15@69735
    13
  where "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f ` A \<subseteq> B"
lp15@69735
    14
lp15@69735
    15
definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50)
lp15@69735
    16
  where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)"
lp15@69735
    17
lp15@69735
    18
lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}"
lp15@69735
    19
  by (auto simp: lepoll_def)
lp15@69735
    20
lp15@69735
    21
lemma eqpoll_iff_card_of_ordIso: "A \<approx> B \<longleftrightarrow> ordIso2 (card_of A) (card_of B)"
lp15@69735
    22
  by (simp add: card_of_ordIso eqpoll_def)
lp15@69735
    23
lp15@69735
    24
lemma eqpoll_finite_iff: "A \<approx> B \<Longrightarrow> finite A \<longleftrightarrow> finite B"
lp15@69735
    25
  by (meson bij_betw_finite eqpoll_def)
lp15@69735
    26
lp15@69735
    27
lemma eqpoll_iff_card:
lp15@69735
    28
  assumes "finite A" "finite B"
lp15@69735
    29
  shows  "A \<approx> B \<longleftrightarrow> card A = card B"
lp15@69735
    30
  using assms by (auto simp: bij_betw_iff_card eqpoll_def)
lp15@69735
    31
lp15@69735
    32
lemma lepoll_antisym:
lp15@69735
    33
  assumes "A \<lesssim> B" "B \<lesssim> A" shows "A \<approx> B"
lp15@69735
    34
  using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
lp15@69735
    35
lp15@69735
    36
lemma lepoll_trans [trans]: "\<lbrakk>A \<lesssim> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
lp15@69735
    37
  apply (clarsimp simp: lepoll_def)
lp15@69735
    38
  apply (rename_tac f g)
lp15@69735
    39
  apply (rule_tac x="g \<circ> f" in exI)
lp15@69735
    40
  apply (auto simp: image_subset_iff inj_on_def)
lp15@69735
    41
  done
lp15@69735
    42
lp15@69735
    43
lemma lepoll_trans1 [trans]: "\<lbrakk>A \<approx> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
lp15@69735
    44
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)
lp15@69735
    45
lp15@69735
    46
lemma lepoll_trans2 [trans]: "\<lbrakk>A \<lesssim> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
lp15@69735
    47
  apply (clarsimp simp: eqpoll_def lepoll_def bij_betw_def)
lp15@69735
    48
  apply (rename_tac f g)
lp15@69735
    49
  apply (rule_tac x="g \<circ> f" in exI)
lp15@69735
    50
  apply (auto simp: image_subset_iff inj_on_def)
lp15@69735
    51
  done
lp15@69735
    52
lp15@69735
    53
lemma eqpoll_sym: "A \<approx> B \<Longrightarrow> B \<approx> A"
lp15@69735
    54
  unfolding eqpoll_def
lp15@69735
    55
  using bij_betw_the_inv_into by auto
lp15@69735
    56
lp15@69735
    57
lemma eqpoll_trans [trans]: "\<lbrakk>A \<approx> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<approx> C"
lp15@69735
    58
  unfolding eqpoll_def using bij_betw_trans by blast
lp15@69735
    59
lp15@69735
    60
lemma eqpoll_imp_lepoll: "A \<approx> B \<Longrightarrow> A \<lesssim> B"
lp15@69735
    61
  unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl)
lp15@69735
    62
lp15@69735
    63
lemma subset_imp_lepoll: "A \<subseteq> B \<Longrightarrow> A \<lesssim> B"
lp15@69735
    64
  by (force simp: lepoll_def)
lp15@69735
    65
lp15@69735
    66
lemma lepoll_iff: "A \<lesssim> B \<longleftrightarrow> (\<exists>g. A \<subseteq> g ` B)"
lp15@69735
    67
  unfolding lepoll_def
lp15@69735
    68
proof safe
lp15@69735
    69
  fix g assume "A \<subseteq> g ` B"
lp15@69735
    70
  then show "\<exists>f. inj_on f A \<and> f ` A \<subseteq> B"
lp15@69735
    71
    by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into)
lp15@69735
    72
qed (metis image_mono the_inv_into_onto)
lp15@69735
    73
lp15@69735
    74
lemma subset_image_lepoll: "B \<subseteq> f ` A \<Longrightarrow> B \<lesssim> A"
lp15@69735
    75
  by (auto simp: lepoll_iff)
lp15@69735
    76
lp15@69735
    77
lemma image_lepoll: "f ` A \<lesssim> A"
lp15@69735
    78
  by (auto simp: lepoll_iff)
lp15@69735
    79
lp15@69735
    80
lemma infinite_le_lepoll: "infinite A \<longleftrightarrow> (UNIV::nat set) \<lesssim> A"
lp15@69735
    81
apply (auto simp: lepoll_def)
lp15@69735
    82
  apply (simp add: infinite_countable_subset)
lp15@69735
    83
  using infinite_iff_countable_subset by blast
lp15@69735
    84
lp15@69735
    85
lemma bij_betw_iff_bijections:
lp15@69735
    86
  "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
lp15@69735
    87
  (is "?lhs = ?rhs")
lp15@69735
    88
proof
lp15@69735
    89
  assume L: ?lhs
lp15@69735
    90
  then show ?rhs
lp15@69735
    91
    apply (rule_tac x="the_inv_into A f" in exI)
lp15@69735
    92
    apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
lp15@69735
    93
    done
lp15@69735
    94
next
lp15@69735
    95
  assume ?rhs
lp15@69735
    96
  then show ?lhs
lp15@69735
    97
    by (auto simp: bij_betw_def inj_on_def image_def; metis)
lp15@69735
    98
qed
lp15@69735
    99
lp15@69735
   100
lemma eqpoll_iff_bijections:
lp15@69735
   101
   "A \<approx> B \<longleftrightarrow> (\<exists>f g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
lp15@69735
   102
    by (auto simp: eqpoll_def bij_betw_iff_bijections)
lp15@69735
   103
lp15@69735
   104
lemma lepoll_restricted_funspace:
lp15@69735
   105
   "{f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A \<and> finite {x. f x \<noteq> k x}} \<lesssim> Fpow (A \<times> B)"
lp15@69735
   106
proof -
lp15@69735
   107
  have *: "\<exists>U \<in> Fpow (A \<times> B). f = (\<lambda>x. if \<exists>y. (x, y) \<in> U then SOME y. (x,y) \<in> U else k x)"
lp15@69735
   108
    if "f ` A \<subseteq> B" "{x. f x \<noteq> k x} \<subseteq> A" "finite {x. f x \<noteq> k x}" for f
lp15@69735
   109
    apply (rule_tac x="(\<lambda>x. (x, f x)) ` {x. f x \<noteq> k x}" in bexI)
lp15@69735
   110
    using that by (auto simp: image_def Fpow_def)
lp15@69735
   111
  show ?thesis
lp15@69735
   112
    apply (rule subset_image_lepoll [where f = "\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x"])
lp15@69735
   113
    using * by (auto simp: image_def)
lp15@69735
   114
qed
lp15@69735
   115
lp15@69874
   116
lemma singleton_lepoll: "{x} \<lesssim> insert y A"
lp15@69874
   117
  by (force simp: lepoll_def)
lp15@69874
   118
lp15@69874
   119
lemma singleton_eqpoll: "{x} \<approx> {y}"
lp15@69874
   120
  by (blast intro: lepoll_antisym singleton_lepoll)
lp15@69874
   121
lp15@69874
   122
lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
lp15@69874
   123
proof safe
lp15@69874
   124
  show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
lp15@69874
   125
    using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
lp15@69874
   126
  show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
lp15@69874
   127
  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
lp15@69874
   128
qed
lp15@69874
   129
lp15@69874
   130
lp15@69735
   131
subsection\<open>The strict relation\<close>
lp15@69735
   132
lp15@69735
   133
lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
lp15@69735
   134
  by (simp add: lepoll_antisym lesspoll_def)
lp15@69735
   135
lp15@69735
   136
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
lp15@69735
   137
by (unfold lesspoll_def, blast)
lp15@69735
   138
lp15@69735
   139
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
lp15@69735
   140
  using eqpoll_imp_lepoll lesspoll_def by blast
lp15@69735
   141
lp15@69735
   142
lemma lesspoll_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
lp15@69735
   143
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
lp15@69735
   144
lp15@69735
   145
lemma lesspoll_trans1 [trans]: "\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
lp15@69735
   146
  by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def)
lp15@69735
   147
lp15@69735
   148
lemma lesspoll_trans2 [trans]: "\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
lp15@69735
   149
  by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def)
lp15@69735
   150
lp15@69735
   151
lemma eq_lesspoll_trans [trans]: "\<lbrakk>X \<approx> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
lp15@69735
   152
  using eqpoll_imp_lepoll lesspoll_trans1 by blast
lp15@69735
   153
lp15@69735
   154
lemma lesspoll_eq_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
lp15@69735
   155
  using eqpoll_imp_lepoll lesspoll_trans2 by blast
lp15@69735
   156
lp15@69735
   157
subsection\<open>Cartesian products\<close>
lp15@69735
   158
lp15@69735
   159
lemma PiE_sing_eqpoll_self: "({a} \<rightarrow>\<^sub>E B) \<approx> B"
lp15@69735
   160
proof -
lp15@69735
   161
  have 1: "x = y"
lp15@69735
   162
    if "x \<in> {a} \<rightarrow>\<^sub>E B" "y \<in> {a} \<rightarrow>\<^sub>E B" "x a = y a" for x y
lp15@69735
   163
    by (metis IntD2 PiE_def extensionalityI singletonD that)
lp15@69735
   164
  have 2: "x \<in> (\<lambda>h. h a) ` ({a} \<rightarrow>\<^sub>E B)" if "x \<in> B" for x
lp15@69735
   165
    using that by (rule_tac x="\<lambda>z\<in>{a}. x" in image_eqI) auto
lp15@69735
   166
  show ?thesis
lp15@69735
   167
  unfolding eqpoll_def bij_betw_def inj_on_def
lp15@69735
   168
  by (force intro: 1 2)
lp15@69735
   169
qed
lp15@69735
   170
lp15@69735
   171
lemma lepoll_funcset_right:
lp15@69735
   172
   "B \<lesssim> B' \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
lp15@69735
   173
  apply (auto simp: lepoll_def inj_on_def)
lp15@69735
   174
  apply (rule_tac x = "\<lambda>g. \<lambda>z \<in> A. f(g z)" in exI)
lp15@69735
   175
  apply (auto simp: fun_eq_iff)
lp15@69735
   176
  apply (metis PiE_E)
lp15@69735
   177
  by blast
lp15@69735
   178
lp15@69735
   179
lemma lepoll_funcset_left:
lp15@69735
   180
  assumes "B \<noteq> {}" "A \<lesssim> A'"
lp15@69735
   181
  shows "A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B"
lp15@69735
   182
proof -
lp15@69735
   183
  obtain b where "b \<in> B"
lp15@69735
   184
    using assms by blast
lp15@69735
   185
  obtain f where "inj_on f A" and fim: "f ` A \<subseteq> A'"
lp15@69735
   186
    using assms by (auto simp: lepoll_def)
lp15@69735
   187
  then obtain h where h: "\<And>x. x \<in> A \<Longrightarrow> h (f x) = x"
lp15@69735
   188
    using the_inv_into_f_f by fastforce
lp15@69735
   189
  let ?F = "\<lambda>g. \<lambda>u \<in> A'. if h u \<in> A then g(h u) else b"
lp15@69735
   190
  show ?thesis
lp15@69735
   191
    unfolding lepoll_def inj_on_def
lp15@69735
   192
  proof (intro exI conjI ballI impI ext)
lp15@69735
   193
    fix k l x
lp15@69735
   194
    assume k: "k \<in> A \<rightarrow>\<^sub>E B" and l: "l \<in> A \<rightarrow>\<^sub>E B" and "?F k = ?F l"
lp15@69735
   195
    then have "?F k (f x) = ?F l (f x)"
lp15@69735
   196
      by simp
lp15@69735
   197
    then show "k x = l x"
lp15@69735
   198
      apply (auto simp: h split: if_split_asm)
lp15@69735
   199
      apply (metis PiE_arb h k l)
lp15@69735
   200
      apply (metis (full_types) PiE_E h k l)
lp15@69735
   201
      using fim k l by fastforce
lp15@69735
   202
  next
lp15@69735
   203
    show "?F ` (A \<rightarrow>\<^sub>E B) \<subseteq> A' \<rightarrow>\<^sub>E B"
lp15@69735
   204
      using \<open>b \<in> B\<close> by force
lp15@69735
   205
  qed
lp15@69735
   206
qed
lp15@69735
   207
lp15@69735
   208
lemma lepoll_funcset:
lp15@69735
   209
   "\<lbrakk>B \<noteq> {}; A \<lesssim> A'; B \<lesssim> B'\<rbrakk> \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B'"
lp15@69735
   210
  by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto
lp15@69735
   211
lp15@69735
   212
lemma lepoll_PiE:
lp15@69735
   213
  assumes "\<And>i. i \<in> A \<Longrightarrow> B i \<lesssim> C i"
lp15@69735
   214
  shows "PiE A B \<lesssim> PiE A C"
lp15@69735
   215
proof -
lp15@69735
   216
  obtain f where f: "\<And>i. i \<in> A \<Longrightarrow> inj_on (f i) (B i) \<and> (f i) ` B i \<subseteq> C i"
lp15@69735
   217
    using assms unfolding lepoll_def by metis
lp15@69735
   218
  then show ?thesis
lp15@69735
   219
    unfolding lepoll_def
lp15@69735
   220
    apply (rule_tac x = "\<lambda>g. \<lambda>i \<in> A. f i (g i)" in exI)
lp15@69735
   221
    apply (auto simp: inj_on_def)
lp15@69735
   222
     apply (rule PiE_ext, auto)
lp15@69735
   223
     apply (metis (full_types) PiE_mem restrict_apply')
lp15@69735
   224
    by blast
lp15@69735
   225
qed
lp15@69735
   226
lp15@69735
   227
lp15@69735
   228
lemma card_le_PiE_subindex:
lp15@69735
   229
  assumes "A \<subseteq> A'" "Pi\<^sub>E A' B \<noteq> {}"
lp15@69735
   230
  shows "PiE A B \<lesssim> PiE A' B"
lp15@69735
   231
proof -
lp15@69735
   232
  have "\<And>x. x \<in> A' \<Longrightarrow> \<exists>y. y \<in> B x"
lp15@69735
   233
    using assms by blast
lp15@69735
   234
  then obtain g where g: "\<And>x. x \<in> A' \<Longrightarrow> g x \<in> B x"
lp15@69735
   235
    by metis
lp15@69735
   236
  let ?F = "\<lambda>f x. if x \<in> A then f x else if x \<in> A' then g x else undefined"
lp15@69735
   237
  have "Pi\<^sub>E A B \<subseteq> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B"
lp15@69735
   238
  proof
lp15@69735
   239
    show "f \<in> Pi\<^sub>E A B \<Longrightarrow> f \<in> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B" for f
lp15@69735
   240
      using \<open>A \<subseteq> A'\<close>
lp15@69735
   241
      by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff)
lp15@69735
   242
  qed
lp15@69735
   243
  then have "Pi\<^sub>E A B \<lesssim> (\<lambda>f. \<lambda>i \<in> A. f i) ` Pi\<^sub>E A' B"
lp15@69735
   244
    by (simp add: subset_imp_lepoll)
lp15@69735
   245
  also have "\<dots> \<lesssim> PiE A' B"
lp15@69735
   246
    by (rule image_lepoll)
lp15@69735
   247
  finally show ?thesis .
lp15@69735
   248
qed
lp15@69735
   249
lp15@69735
   250
lp15@69735
   251
lemma finite_restricted_funspace:
lp15@69735
   252
  assumes "finite A" "finite B"
lp15@69735
   253
  shows "finite {f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A}" (is "finite ?F")
lp15@69735
   254
proof (rule finite_subset)
lp15@69735
   255
  show "finite ((\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x) ` Pow(A \<times> B))" (is "finite ?G")
lp15@69735
   256
    using assms by auto
lp15@69735
   257
  show "?F \<subseteq> ?G"
lp15@69735
   258
  proof
lp15@69735
   259
    fix f
lp15@69735
   260
    assume "f \<in> ?F"
lp15@69735
   261
    then show "f \<in> ?G"
lp15@69735
   262
      by (rule_tac x="(\<lambda>x. (x,f x)) ` {x. f x \<noteq> k x}" in image_eqI) (auto simp: fun_eq_iff image_def)
lp15@69735
   263
  qed
lp15@69735
   264
qed
lp15@69735
   265
lp15@69735
   266
lp15@69735
   267
proposition finite_PiE_iff:
lp15@69735
   268
   "finite(PiE I S) \<longleftrightarrow> PiE I S = {} \<or> finite {i \<in> I. ~(\<exists>a. S i \<subseteq> {a})} \<and> (\<forall>i \<in> I. finite(S i))"
lp15@69735
   269
 (is "?lhs = ?rhs")
lp15@69735
   270
proof (cases "PiE I S = {}")
lp15@69735
   271
  case False
lp15@69735
   272
  define J where "J \<equiv> {i \<in> I. \<nexists>a. S i \<subseteq> {a}}"
lp15@69735
   273
  show ?thesis
lp15@69735
   274
  proof
lp15@69735
   275
    assume L: ?lhs
lp15@69735
   276
    have "infinite (Pi\<^sub>E I S)" if "infinite J"
lp15@69735
   277
    proof -
lp15@69735
   278
      have "(UNIV::nat set) \<lesssim> (UNIV::(nat\<Rightarrow>bool) set)"
lp15@69735
   279
      proof -
lp15@69735
   280
        have "\<forall>N::nat set. inj_on (=) N"
lp15@69735
   281
          by (simp add: inj_on_def)
lp15@69735
   282
        then show ?thesis
lp15@69735
   283
          by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum)
lp15@69735
   284
      qed
lp15@69735
   285
      also have "\<dots> = (UNIV::nat set) \<rightarrow>\<^sub>E (UNIV::bool set)"
lp15@69735
   286
        by auto
lp15@69735
   287
      also have "\<dots> \<lesssim> J \<rightarrow>\<^sub>E (UNIV::bool set)"
lp15@69735
   288
        apply (rule lepoll_funcset_left)
lp15@69735
   289
        using infinite_le_lepoll that by auto
lp15@69735
   290
      also have "\<dots> \<lesssim> Pi\<^sub>E J S"
lp15@69735
   291
      proof -
lp15@69735
   292
        have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and "\<forall>a. \<not> S i \<subseteq> {a}" for i
lp15@69735
   293
        proof -
lp15@69735
   294
          obtain a b where "{a,b} \<subseteq> S i" "a \<noteq> b"
lp15@69735
   295
            by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
lp15@69735
   296
          then show ?thesis
lp15@69735
   297
            apply (clarsimp simp: lepoll_def inj_on_def)
lp15@69735
   298
            apply (rule_tac x="\<lambda>x. if x then a else b" in exI, auto)
lp15@69735
   299
            done
lp15@69735
   300
        qed
lp15@69735
   301
        show ?thesis
lp15@69735
   302
          by (auto simp: * J_def intro: lepoll_PiE)
lp15@69735
   303
      qed
lp15@69735
   304
      also have "\<dots> \<lesssim> Pi\<^sub>E I S"
lp15@69735
   305
        using False by (auto simp: J_def intro: card_le_PiE_subindex)
lp15@69735
   306
      finally have "(UNIV::nat set) \<lesssim> Pi\<^sub>E I S" .
lp15@69735
   307
      then show ?thesis
lp15@69735
   308
        by (simp add: infinite_le_lepoll)
lp15@69735
   309
    qed
lp15@69735
   310
    moreover have "finite (S i)" if "i \<in> I" for i
lp15@69735
   311
    proof (rule finite_subset)
lp15@69735
   312
      obtain f where f: "f \<in> PiE I S"
lp15@69735
   313
        using False by blast
lp15@69735
   314
      show "S i \<subseteq> (\<lambda>f. f i) ` Pi\<^sub>E I S"
lp15@69735
   315
      proof
lp15@69735
   316
        show "s \<in> (\<lambda>f. f i) ` Pi\<^sub>E I S" if "s \<in> S i" for s
lp15@69735
   317
          using that f \<open>i \<in> I\<close>
lp15@69735
   318
          by (rule_tac x="\<lambda>j. if j = i then s else f j" in image_eqI) auto
lp15@69735
   319
      qed
lp15@69735
   320
    next
lp15@69735
   321
      show "finite ((\<lambda>x. x i) ` Pi\<^sub>E I S)"
lp15@69735
   322
        using L by blast
lp15@69735
   323
    qed
lp15@69735
   324
    ultimately show ?rhs
lp15@69735
   325
      using L
lp15@69735
   326
      by (auto simp: J_def False)
lp15@69735
   327
  next
lp15@69735
   328
    assume R: ?rhs
lp15@69735
   329
    have "\<forall>i \<in> I - J. \<exists>a. S i = {a}"
lp15@69735
   330
      using False J_def by blast
lp15@69735
   331
    then obtain a where a: "\<forall>i \<in> I - J. S i = {a i}"
lp15@69735
   332
      by metis
lp15@69735
   333
    let ?F = "{f. f ` J \<subseteq> (\<Union>i \<in> J. S i) \<and> {i. f i \<noteq> (if i \<in> I then a i else undefined)} \<subseteq> J}"
lp15@69735
   334
    have *: "finite (Pi\<^sub>E I S)"
lp15@69735
   335
      if "finite J" and "\<forall>i\<in>I. finite (S i)"
lp15@69735
   336
    proof (rule finite_subset)
lp15@69735
   337
      show "Pi\<^sub>E I S \<subseteq> ?F"
lp15@69735
   338
        apply safe
lp15@69735
   339
        using J_def apply blast
lp15@69735
   340
        by (metis DiffI PiE_E a singletonD)
lp15@69735
   341
      show "finite ?F"
lp15@69735
   342
      proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
lp15@69735
   343
        show "finite (\<Union> (S ` J))"
lp15@69735
   344
          using that J_def by blast
lp15@69735
   345
      qed
lp15@69735
   346
  qed
lp15@69735
   347
  show ?lhs
lp15@69735
   348
      using R by (auto simp: * J_def)
lp15@69735
   349
  qed
lp15@69735
   350
qed auto
lp15@69735
   351
lp15@69735
   352
lp15@69735
   353
corollary finite_funcset_iff:
lp15@69735
   354
  "finite(I \<rightarrow>\<^sub>E S) \<longleftrightarrow> (\<exists>a. S \<subseteq> {a}) \<or> I = {} \<or> finite I \<and> finite S"
lp15@69735
   355
  apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD)
lp15@69735
   356
  using finite.simps by auto
lp15@69735
   357
lp15@69735
   358
end