induction_on — Mathlib

English

An induction principle: to prove a property for any element of the associated quotient, it suffices to prove it for representatives of the form of a single generator.

Русский

Принцип индукции: чтобы доказать свойство для любого элемента вAssocQuotient α, достаточно доказать его для представителей вида от одного генератора.

LaTeX

$$$\forall C: \mathrm{AssocQuotient}(\alpha) \to \mathrm{Prop},\ (\forall a:\alpha, C(\mathrm{of}(a))) \to \forall x, C(x)$$$

Lean4

@[to_additive (attr := elab_as_elim, induction_eliminator)]
protected theorem induction_on {C : AssocQuotient α → Prop} (x : AssocQuotient α) (ih : ∀ x, C (of x)) : C x :=
  Quot.induction_on x ih

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