coe_intCast

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

The integer casting respects the underlying function: the integer cast of a bounded function is the function itself.

Русский

Целочисленное приведение к функции сохраняет её как есть.

LaTeX

$$$\\forall n \\in \\mathbb{Z}, \\ ((n : α →ᵇ R) : α → R) = n$$$

Lean4

@[simp, norm_cast]
theorem coe_intCast (n : ℤ) : ((n : α →ᵇ R) : α → R) = n :=
  rfl

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

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

Разделы

Аффилиация

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