induction_on — Mathlib

English

If a property holds for every representative a of a quotient q, then it holds for q itself.

Русский

Если свойство верно для каждого представителя a квоты q, то оно верно и для самой квоты q.

LaTeX

$$$$\forall {\alpha : Sort*} {r : \alpha \to \alpha \to Prop} {\beta : Quot r \to Prop} (q : Quot r), (\forall a, \beta (Quot.mk r a)) \rightarrow \beta q.$$$$

Lean4

@[elab_as_elim]
protected theorem induction_on {α : Sort*} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r)
    (h : ∀ a, β (Quot.mk r a)) : β q :=
  ind h q

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