w_cases — Mathlib

English

A direct corollary of the induction principle: if a predicate holds for every constructor, then it holds for all W-trees.

Русский

Следствие индукционного принципа: если предикат верен для каждого конструктора, то он верен для всех деревьев W.

LaTeX

$$$\forall x,\, C\,x\quad\text{whenever }(\forall a\, f'\, f,\, C(wMk\, a\, f'\, f)).$$$

Lean4

theorem w_cases {α : TypeVec n} {C : P.W α → Prop}
    (ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), C (P.wMk a f' f)) : ∀ x, C x :=
  P.w_ind fun a f' f _ih' => ih a f' f

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