induction_on — Mathlib

English

If a property holds for mk a for every a, then it holds for every q in Trunc α.

Русский

Если свойство верно дляmk a для каждого a, то оно верно и для любого q в Trunc α.

LaTeX

$$$\\big( \\forall a:\\, \\alpha,\\beta(\\mathrm{mk}\\,a) \\big) \\Rightarrow \\forall q:\\, \\mathrm{Trunc}(\\alpha),\\ \\beta(q)$$$

Lean4

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

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