# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1598890727 -3600
# Node ID 6b620d91e8cc9b27ace1775c1b1d283ee122d7d9
# Parent  4710dd5093a35d206f15e32d3b0d992145636847
a new lemma

diff -r 4710dd5093a3 -r 6b620d91e8cc src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Aug 31 16:48:31 2020 +0200
+++ b/src/HOL/Library/Ramsey.thy	Mon Aug 31 17:18:47 2020 +0100
@@ -18,8 +18,11 @@
 lemma nsets_mono: "A \<subseteq> B \<Longrightarrow> nsets A n \<subseteq> nsets B n"
   by (auto simp: nsets_def)
 
+lemma nsets_Pi_contra: "A' \<subseteq> A \<Longrightarrow> Pi ([A]\<^bsup>n\<^esup>) B \<subseteq> Pi ([A']\<^bsup>n\<^esup>) B"
+  by (auto simp: nsets_def)
+
 lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})"
-by (auto simp: nsets_def card_2_iff)
+  by (auto simp: nsets_def card_2_iff)
 
 lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})"
   by (auto simp: nsets_2_eq)