cons_induction_on — Mathlib

English

A specialized induction principle: proving a property for all Finset α by starting from ∅ and repeatedly inserting new elements from α.

Русский

Уточнённая индукция по Finset α: доказать свойство для всех Finset α, начиная с ∅ и добавляя новые элементы.

LaTeX

$$$\\text{cons_induction_on}(\\text{S}, \\text{empty}, \\text{cons})$ реализует базовый принцип, аналогичный предыдущему$$

Lean4

@[elab_as_elim]
theorem cons_induction_on {α : Type*} {motive : Finset α → Prop} (s : Finset α) (empty : motive ∅)
    (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (cons a s h)) : motive s :=
  cons_induction empty cons s

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