natCast_apply — Mathlib

English

If each fibre π(a) supports a numeral n via NatCast, then (n : ∀ a, π(a)) is the constant function a ↦ (OfNat or NatCast) n.

Русский

Если каждый слой π(a) поддерживает числовую константу n через NatCast, то (n : ∀ a, π(a)) является константной функцией a ↦ n.

LaTeX

$$$$ (n : \forall a, \pi a) a = n $$$$

Lean4

@[simp]
theorem natCast_apply (n : ℕ) (a : α) : (n : ∀ a, π a) a = n :=
  rfl

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