A nice cardinality lemma
authorpaulson <lp15@cam.ac.uk>
Mon, 03 May 2021 21:49:30 +0100
changeset 73876 58aed6f71f90
parent 73875 0c8d6bec6491
child 73877 b4b70d13c995
A nice cardinality lemma
src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon May 03 19:06:33 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Mon May 03 21:49:30 2021 +0100
@@ -1811,6 +1811,10 @@
     (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
   by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD)
 
+lemma card_Suc_eq_finite:
+  "card A = Suc k \<longleftrightarrow> (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> finite B)"
+  unfolding card_Suc_eq using card_gt_0_iff by fastforce
+
 lemma card_1_singletonE:
   assumes "card A = 1"
   obtains x where "A = {x}"