blob: 9a74ffcce7ed8c2b2e706d58d773bb4387c9c9b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
import Mathlib.Tactic
namespace Finset.Nonempty
theorem induction
{α : Type} {motive : Finset α → Prop} [DecidableEq α]
(single : ∀ (a : α), motive {a})
(insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s))
: ∀ s, Finset.Nonempty s → motive s := by
intro S
induction' S using Finset.induction
· simp
· expose_names
intro _
by_cases h : (Finset.Nonempty s)
· apply insert
· assumption
· apply h_1; assumption
· simp only [not_nonempty_iff_eq_empty] at h
rw [h]
apply single
end Finset.Nonempty
|
