# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1580137097 0
# Node ID 3ab52e4a8b456d3ea35ec351da0e6f294558d8e2
# Parent  f2b783abfbe71694b263c5984da0c9e0a4fd2656
Two lemmas about nsets

diff -r f2b783abfbe7 -r 3ab52e4a8b45 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Jan 27 14:32:43 2020 +0000
+++ b/src/HOL/Library/Ramsey.thy	Mon Jan 27 14:58:17 2020 +0000
@@ -62,6 +62,24 @@
 lemma nsets_one: "nsets A (Suc 0) = (\<lambda>x. {x}) ` A"
   using card_eq_SucD by (force simp: nsets_def)
 
+lemma inj_on_nsets:
+  assumes "inj_on f A"
+  shows "inj_on (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>)"
+  using assms unfolding nsets_def
+  by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq)
+
+lemma bij_betw_nsets:
+  assumes "bij_betw f A B"
+  shows "bij_betw (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>) ([B]\<^bsup>n\<^esup>)"
+proof -
+  have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>"
+    using assms
+    apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset)
+    by (metis card_image inj_on_finite order_refl subset_image_inj)
+  with assms show ?thesis
+    by (auto simp: bij_betw_def inj_on_nsets)
+qed
+
 subsubsection \<open>Partition predicates\<close>
 
 definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool"