English
To prove a property for a nonempty Finset s, it suffices to prove it for singletons and to show that if it holds for nonempty t, then it also holds after inserting an element.
Русский
Чтобы доказать свойство для ненулевого Finset s, достаточно доказать его для единичных множеств и показать, что если свойство верно для ненулевого t, то верно и после вставки элемента.
LaTeX
$$@[elab_as_elim] theorem cons_induction {α} {motive : ∀ s : Finset α, s.Nonempty → Prop} (singleton : ∀ a, motive { a } (singleton_nonempty _)) (cons : ∀ a s (h : a ∉ s) (hs), motive s hs → motive (Finset.cons a s h) (cons_nonempty h)) {s : Finset α} (hs : s.Nonempty) : motive s hs$$
Lean4
/-- To prove a proposition about a nonempty `s : Finset α`, it suffices to show it holds for all
singletons and that if it holds for nonempty `t : Finset α`, then it also holds for the `Finset`
obtained by inserting an element in `t`. -/
@[elab_as_elim]
theorem cons_induction {α : Type*} {motive : ∀ s : Finset α, s.Nonempty → Prop}
(singleton : ∀ a, motive { a } (singleton_nonempty _))
(cons : ∀ a s (h : a ∉ s) (hs), motive s hs → motive (Finset.cons a s h) (cons_nonempty h)) {s : Finset α}
(hs : s.Nonempty) : motive s hs := by
induction s using Finset.cons_induction with
| empty => exact (not_nonempty_empty hs).elim
| cons a t ha h =>
obtain rfl | ht := t.eq_empty_or_nonempty
· exact singleton a
·
exact
cons a t ha ht
(h ht)
-- We use a fresh `α` here to exclude the unneeded `DecidableEq α` instance from the section.
