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

refactor(library/data/finste/basic): rename non_empty_of_card_succ to ne_empty_of_card_eq_succ

Browse source
This commit is contained in:
Jeremy Avigad 2015-07-11 12:09:36 +10:00 committed by Leonardo de Moura
parent d443b25dee
commit 9810105a2a
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -213,7 +213,7 @@ decidable.by_cases
(assume H : a ∈ s, by rewrite [card_insert_of_mem H]; apply le_succ)
(assume H : a ∉ s, by rewrite [card_insert_of_not_mem H])
lemma non_empty_of_card_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
lemma ne_empty_of_card_eq_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
by intros; substvars; contradiction
protected theorem induction [recursor 6] {P : finset A → Prop}

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

@ -126,7 +126,7 @@ section deceqA
intros [H1, H2],
rewrite [Union_insert, H2 _ !mem_insert],
cases (decidable.em (s' = ∅)) with [seq, sne],
{rewrite [seq, Union_empty, union_empty] },
{rewrite [seq, Union_empty, union_empty]},
have H3 : ∀ x, x ∈ s' → f x = t, from (λ x H', H2 x (mem_insert_of_mem _ H')),
rewrite [IH sne H3, union_self]
end