equal
deleted
inserted
replaced
2052 apply(auto) |
2052 apply(auto) |
2053 apply(subst card_insert) |
2053 apply(subst card_insert) |
2054 apply(auto intro:ccontr) |
2054 apply(auto intro:ccontr) |
2055 done |
2055 done |
2056 |
2056 |
|
2057 lemma card_le_Suc_iff: "finite A \<Longrightarrow> |
|
2058 Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)" |
|
2059 by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff |
|
2060 dest: subset_singletonD split: nat.splits if_splits) |
|
2061 |
2057 lemma finite_fun_UNIVD2: |
2062 lemma finite_fun_UNIVD2: |
2058 assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)" |
2063 assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)" |
2059 shows "finite (UNIV :: 'b set)" |
2064 shows "finite (UNIV :: 'b set)" |
2060 proof - |
2065 proof - |
2061 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" |
2066 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" |