induction_on — Mathlib

English

If s is subsingleton, and p holds for ∅ and for all singleton sets {x}, then p holds for s.

Русский

Если s субоднозначно, и свойство p верно для пустого множества и для всех множеств вида {x}, то p верно и для s.

LaTeX

$$$ p \; ∅ \; \land \; (\forall x, p\{x\}) \Rightarrow p\,s $$$

Lean4

theorem induction_on {p : Set α → Prop} (hs : s.Subsingleton) (he : p ∅) (h₁ : ∀ x, p { x }) : p s :=
  by
  rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
  exacts [he, h₁ _]

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