induction_on — Mathlib

English

Same as induction, but presented as a reusable lemma: induction_on s empty cons := p s.

Русский

То же, что индукция, но представлено как полезная лемма: induction_on s empty cons.

LaTeX

$$Induction_on {p : Multiset α → Prop} (s) (empty) (cons) : p s$$

Lean4

@[elab_as_elim]
protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (empty : p 0)
    (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : p s :=
  Multiset.induction empty cons s

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