From 339a7334f87298ed93aed84986fce797d22146ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jul 2015 13:44:47 -0700 Subject: [PATCH] feat(library/data/finset/card): add exists_two_of_card_gt_one --- library/data/finset/card.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index d4876e26de..f0520b0bb9 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -209,4 +209,18 @@ finset.induction_on s card_union_of_disjoint H8, H6]) end deceqB +lemma exists_two_of_card_gt_one {s : finset A} : 1 < card s → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b := +begin + intro h, + induction s with a s nain ih₁, + {exact absurd h dec_trivial}, + {induction s with b s nbin ih₂, + {exact absurd h dec_trivial}, + clear ih₁ ih₂, + existsi a, existsi b, split, + {apply mem_insert}, + split, + {apply mem_insert_of_mem _ !mem_insert}, + {intro aeqb, subst a, exact absurd !mem_insert nain}} +end end finset