Theorems · Theorem · order theory

Set.Finite.induction_on_subset

∀ {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite),
  motive ∅ ⋯ →
    (∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) → motive s hs

Induction principle for finite sets: To prove a property C of a finite set s, it's enough to prove for the empty set and to prove that C t → C ({a} ∪ t) for all t ⊆ s. This is analogous to Finset.induction_on'. See also Set.Finite.induction_on for the version requiring motive t → motive ({a} ∪ t) for all t.

Defined in

Mathlib.Data.Set.Finite.Basic

Cited by

2 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound