src/HOL/Finite_Set.thy
changeset 44744 bdf8eb8f126b
parent 43991 f4a7697011c5
child 44835 ff6b9eb9c5ef
equal deleted inserted replaced
44743:804dfa6d35b6 44744:bdf8eb8f126b
  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))"