induction_on — Mathlib

English

Let C be a property of elements of AdjoinRoot f. If C holds for every mk f p with p ranging over all polynomials in R[X], then C holds for every element x of AdjoinRoot f.

Русский

Пусть C — свойство над элементами AdjoinRoot f. Если для каждого p ∈ R[X] верно C(mk f p), то верно C для любого элемента x ∈ AdjoinRoot f.

LaTeX

$$\\forall {C : AdjoinRoot f \\to Prop} (x : AdjoinRoot f) (ih : \\forall p : R[X], C (mk f p)), C x$$

Lean4

@[elab_as_elim]
theorem induction_on {C : AdjoinRoot f → Prop} (x : AdjoinRoot f) (ih : ∀ p : R[X], C (mk f p)) : C x :=
  Quotient.inductionOn' x ih

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