moved from AFP/Gromov
Fri, 19 Jan 2018 12:14:48 +0100
changeset 67457 4b921bb461f6
parent 67456 7895c159d7b1
child 67458 e090941f9f42
moved from AFP/Gromov
--- a/src/HOL/Finite_Set.thy	Fri Jan 19 08:28:08 2018 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 19 12:14:48 2018 +0100
@@ -1743,6 +1743,24 @@
   then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
+text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets
+and to show that their cardinalities are uniformly bounded. This possibility is formalized in
+the next criterion.\<close>
+lemma finite_if_finite_subsets_card_bdd:
+  assumes "\<And>G. G \<subseteq> F \<Longrightarrow> finite G \<Longrightarrow> card G \<le> C"
+  shows "finite F \<and> card F \<le> C"
+proof (cases "finite F")
+  case False
+  obtain n::nat where n: "n > max C 0" by auto
+  obtain G where G: "G \<subseteq> F" "card G = n" using infinite_arbitrarily_large[OF False] by auto
+  hence "finite G" using \<open>n > max C 0\<close> using card_infinite gr_implies_not0 by blast
+  hence False using assms G n not_less by auto
+  thus ?thesis ..
+  case True thus ?thesis using assms[of F] by auto
 subsubsection \<open>Cardinality of image\<close>