const_succ — Mathlib

English

@[simp] The successor case for OfArity: OfArity α β (n.succ) = α → OfArity α β n.

Русский

@[simp] Пример для successor: OfArity α β (n.succ) = α → OfArity α β n.

LaTeX

$$$$\mathrm{OfArity.const\_succ}(\alpha,\beta,n) : \mathrm{OfArity}(\alpha,\beta, n.succ) = (\alpha \to \mathrm{OfArity}(\alpha,\beta,n)). $$$$

Lean4

@[simp]
theorem const_succ (α : Type u) {β : Type u} (b : β) (n : ℕ) : const α b n.succ = fun _ => const _ b n :=
  FromTypes.const_succ (fun _ => α) b

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