inductionOn — Mathlib

English

For any f : Sym2 α → Prop, if f holds for all pairs (x,y), then f holds for any i ∈ Sym2 α.

Русский

Для любого f : Sym2 α → Prop, если выполняется для каждого пары (x,y), тогда выполняется и для любого i ∈ Sym2 α.

LaTeX

$$$$ \forall f : Sym2\alpha \to Prop, (\forall x,y, f(\mathrm{Sym2.mk}\{fst := x, snd := y\})) \to f\,i. $$$$

Lean4

@[elab_as_elim]
protected theorem inductionOn {f : Sym2 α → Prop} (i : Sym2 α) (hf : ∀ x y, f s(x, y)) : f i :=
  i.ind hf

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