michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/finset/basic): rename theorem

Browse source
This commit is contained in:
Jeremy Avigad 2015-12-31 10:50:11 -08:00 committed by Leonardo de Moura
parent a28ded641c
commit 8a00a431e8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/finset/basic.lean
View file

@ -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},