coe_smul

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.coe_smul

← MathLib Explorer

English

For r in R and f in C₀(α,β), (r • f) x = r • f x for all x.

Русский

Для любого r∈R и f∈C₀(α,β) выполняется (r•f) x = r•f x для всех x.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_smul [Zero β] {R : Type*} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] (r : R) (f : C₀(α, β)) :
    ⇑(r • f) = r • ⇑f :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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