From 8a00a431e87353211003d87d4b238bfad33bc545 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 31 Dec 2015 10:50:11 -0800 Subject: [PATCH] refactor(library/data/finset/basic): rename theorem --- library/data/finset/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index cb2abb34d8..2359b8dc3d 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -251,7 +251,7 @@ protected theorem induction_on {P : finset A → Prop} (s : finset A) P s := finset.induction H1 H2 s -theorem exists_of_not_empty {s : finset A} : s ≠ ∅ → ∃ a : A, a ∈ s := +theorem exists_me_of_ne_empty {s : finset A} : s ≠ ∅ → ∃ a : A, a ∈ s := begin induction s with a s nin ih, {intro h, exact absurd rfl h},