inductionOn — Mathlib

English

The presented monoid satisfies an induction principle: to prove a property δ on any element, it suffices to prove it on representatives mk rels a.

Русский

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

LaTeX

$$$\\forall q, \\delta(q) \\,\\text{ if } \\forall a, \\delta(\\mathrm{mk}\\,\\text{rels}, a)$$$

Lean4

@[to_additive (attr := elab_as_elim), induction_eliminator]
protected theorem inductionOn {δ : P₁ → Prop} (q : P₁) (h : ∀ a, δ (mk rels₁ a)) : δ q :=
  Quotient.ind h q

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