ind — Mathlib

English

An induction principle for MulArchimedeanClass: every motive holds if it holds on representatives mk a.

Русский

Принцип индукции для MulArchimedeanClass: свойство верно, если оно верно для представлений mk a.

LaTeX

$$$\forall x, P(x)$, если $P(mk(a))$ для всех a ∈ M.$$

Lean4

/-- An induction principle for `MulArchimedeanClass`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator) /-- An induction principle for `ArchimedeanClass` -/
    ]
theorem ind {motive : MulArchimedeanClass M → Prop} (mk : ∀ a, motive (.mk a)) : ∀ x, motive x :=
  Antisymmetrization.ind _ mk

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