inductionOn — Mathlib

English

Let p be a property on ZFSet. If for every x, whenever p holds for all elements y ∈ x, then p holds for x, then p(x) holds.

Русский

Пусть p — свойство над ZFSet. Если для каждого x верно: если p выполняется для всех элементов y ∈ x, тогда p выполняется и для x, то для данного x справедливо p(x).

LaTeX

$$$\\forall p:\\\\mathrm{ZFSet} \\to \\mathrm{Prop},\\ (\\\\forall x:\\\\mathrm{ZFSet},\\ (\\\\forall y \\in x, p(y)) \\rightarrow p(x)) \\rightarrow p(x)$$$

Lean4

/-- Induction on the `∈` relation. -/
@[elab_as_elim]
theorem inductionOn {p : ZFSet → Prop} (x) (h : ∀ x, (∀ y ∈ x, p y) → p x) : p x :=
  mem_wf.induction x h

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