ofNat_def — Mathlib

English

For n and a, the element of the Pi-type corresponding to OfNat is the value provided by OfNat in each fiber; i.e., (OfNat n) equals the function a ↦ (inst a).ofNat n.

Русский

Для данного n элемент Pi-типа соответствует значению, задаваемому OfNat в каждом стержне; то есть OfNat n = функция a ↦ (inst a).ofNat n.

LaTeX

$$$$ (ofNat(n) : \forall a, \pi a) = \lambda a. (inst a).ofNat n $$$$

Lean4

theorem ofNat_def (n : ℕ) [∀ i, OfNat (π i) n] : (ofNat(n) : ∀ a, π a) = fun _ ↦ ofNat(n) :=
  rfl

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