natCast_def

Mathlib.Data.Nat.Cast.Basic

URI: https://scilib.ai/kg/mathlib#Pi.natCast_def

English

For any α, π and [∀ a, NatCast (π(a))], natCast (n) in the Pi-type equals the constant function a ↦ ↑n.

Русский

Для любых α, π и [∀ a, NatCast (π(a))], natCast(n) в Pi-типе равен константной функции a ↦ ↑n.

LaTeX

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

Lean4

theorem natCast_def (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru