Theorems · Theorem · order theory

Finset.induction_on_max

∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : DecidableEq α] {motive : Finset α → Prop} (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (insert a s)) → motive s

Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that: * it is true on the empty Finset, * for every s : Finset α and an element a strictly greater than all elements of s, p s implies p (insert a s).

Defined in

Mathlib.Data.Finset.Max

Cited by

4 results in Mathlib

Foundations

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

Assumes

LinearOrderDecidableEq