induction — Mathlib

English

For any property p of multisets, if p(0) holds and p(s) implies p(a ::ₘ s) for all a, then p(s) holds for every s.

Русский

Для любого свойства p над мультисетами, если выполняется p(0) и p(s) ⇒ p(a ::ₘ s) для всех a, то p(s) верно для любого s.

LaTeX

$$∀ {p : Multiset α → Prop}, p 0 → (∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) → ∀ s, p s$$

Lean4

@[elab_as_elim]
protected theorem induction {p : Multiset α → Prop} (empty : p 0)
    (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : ∀ s, p s := by rintro ⟨l⟩;
  induction l with
  | nil => exact empty
  | cons _ _ ih => exact cons _ _ ih

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