induction_on_min — Mathlib

English

Alternative formulation of induction on max for Finsets with predicate P: base case P(∅); step: for a not in s with elements below a, P(s) implies P(insert a s). Then P(s) holds for all s.

Русский

Альтернативная формулировка индукции по максимуму для Finset с предикатом P: основание P(пустое); шаг: для a не в s и всех x ∈ s x < a, P(s) ⇒ P(вставить a в s). Тогда P выполняется для всех s.

LaTeX

$$$ \\forall s\\; [\, 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 less than all elements of `s`, `p s`
  implies `p (insert a s)`. -/
@[elab_as_elim]
theorem induction_on_min [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅)
    (step : ∀ a s, (∀ x ∈ s, a < x) → p s → p (insert a s)) : p s :=
  @induction_on_max αᵒᵈ _ _ _ s h0 step

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