coe_zsmul

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

For any integer r, the r-multiple of f is evaluated pointwise: (r · f)(x) = r · f(x).

Русский

Для любого целого r умножение f на r выполняется по точкам: (r · f)(x) = r · f(x).

LaTeX

$$$ (r \cdot f)(x) = r \cdot f(x) $$$

Lean4

@[simp]
theorem coe_zsmul (r : ℤ) (f : α →ᵇ β) : ⇑(r • f) = r • ⇑f :=
  rfl

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

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

Разделы

Аффилиация

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