ind — Mathlib

English

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

Русский

Для любого f : Sym2 α → Prop, если f выполняется для всех Sym2.mk x y, то f выполняется и для любого i ∈ Sym2 α.

LaTeX

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

Lean4

@[elab_as_elim, cases_eliminator, induction_eliminator]
protected theorem ind {f : Sym2 α → Prop} (h : ∀ x y, f s(x, y)) : ∀ i, f i :=
  Quot.ind <| Prod.rec <| h

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