Update putnam_2013_b5.thy

trishullab · Jul 15, 2024 · 90c40f3 · 90c40f3
1 parent fd75e4c
commit 90c40f3
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/isabelle/putnam_2013_b5.thy b/isabelle/putnam_2013_b5.thy
@@ -10,5 +10,6 @@ theorem putnam_2013_b5:
     and kinX: "k \<in> {1..n}"
   defines "fiter \<equiv> \<lambda>f. (f ` {1..n} \<subseteq> {1..n} \<and> (\<forall>x::nat\<in>{1..n}. \<exists>j::nat. (f^^j) x \<le> k)) \<and> (\<forall>x::nat > n. f x = 0) \<and> f 0 = 0"
   shows "card {f::nat\<Rightarrow>nat. fiter f} = k * n^(n-1)"
+  sorry
 
 end