Theorems · Theorem · order theory

Set.Finite.induction_on

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

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

Defined in

Mathlib.Data.Set.Finite.Basic

Cited by

39 results in Mathlib

Foundations

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