invSet_recOn — Mathlib

English

A recursion principle for invSet: if p holds for 0 and is closed under the inverse-step construction, then p holds for all elements of invSet(a).

Русский

Рекурсивный принцип для invSet: если p верно для 0 и сохраняется при шаге инверсии, то p верно для всех элементов invSet(a).

LaTeX

$$$\forall p:\Nimber\to\text{Prop},\ (p(0)) \land\Big(\forall a'

Lean4

/-- A recursion principle for `invSet`. -/
@[elab_as_elim]
theorem invSet_recOn {p : Nimber → Prop} (a : Nimber) (h0 : p 0)
    (hi : ∀ a' < a, a' ≠ 0 → ∀ b, p b → p (invAux a' * (1 + (a + a') * b))) (x : Nimber) (hx : x ∈ invSet a) : p x :=
  by
  revert x
  rw [invSet]
  exact Set.sInter_subset_of_mem ⟨h0, hi⟩

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