Theorems · Theorem · order theory

Set.Finite.induction_to

∀ {α : Type u} {C : Set α → Prop} {S : Set α},
  S.Finite → ∀ S0 ⊆ S, C S0 → (∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) → C S

Induction up to a finite set S.

Defined in

Mathlib.Data.Set.Finite.Lemmas

Cited by

1 results in Mathlib

Foundations

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