induction_on_max — Mathlib

English

Induction principle for Finsets in a linearly ordered type: if P holds for the empty Finset and whenever a is greater than all elements of s and P(s) holds then P(insert a s) holds, then P holds for all Finsets.

Русский

Принцип индукции по максимуму для конечных множеств в линейно упорядоченном типе: если справедливо P(пустое M) и если для любого a, большего любого элемента множества s, P(s) ⇒ P(вставить a в s), тогда P выполняется для всех Finset.

LaTeX

$$$ \\forall s \\in \\mathrm{Finset}(\\alpha):\\ P(s)\\;\\text{where}\; P(\\varnothing) \\,\\wedge\\, (\\forall a\\,s\\, (\\forall x\\in s, x

Lean4

/-- Induction principle for `Finset`s 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)`. -/
@[elab_as_elim]
theorem induction_on_max [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅)
    (step : ∀ a s, (∀ x ∈ s, x < a) → p s → p (insert a s)) : p s :=
  by
  induction s using Finset.eraseInduction with
  | _ s ih
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · exact h0
  · have H : s.max' hne ∈ s := max'_mem s hne
    rw [← insert_erase H]
    exact step _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

Похожие утверждения