natCast_apply

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.natCast_apply

English

For any natural number n, the n-th constant function evaluates at x to n.

Русский

Для любого натурального числа n соответствующая константная функция принимает значение n в любом x.

LaTeX

$$$\forall n \in \mathbb{N},\; (n: \alpha \to^{\mathrm{b}} \beta)(x) = n$$$

Lean4

@[simp]
theorem natCast_apply [NatCast β] (n : ℕ) (x : α) : (n : α →ᵇ β) x = n :=
  rfl

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

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

Разделы

Аффилиация

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