ofNat_apply — Mathlib

English

The application of the Pi-instantiated OfNat at n to a equals the OfNat(n) for a, i.e., ((Pi.instOfNat n).ofNat n) a = ((inst a).ofNat n).

Русский

Применение инстанса OfNat в Pi на n к аргументу a даёт тот же результат, что и инстанс OfNat в π(a) на n.

LaTeX

$$$$ ((Pi.instOfNat n).ofNat n) a = ((inst a).ofNat n) $$$$

Lean4

@[simp]
theorem ofNat_apply (n : ℕ) [∀ i, OfNat (π i) n] (a : α) : (ofNat(n) : ∀ a, π a) a = ofNat(n) :=
  rfl

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