enorm_smul

Mathlib.Analysis.Normed.MulAction

URI: https://scilib.ai/kg/mathlib#enorm_smul

English

For all r ∈ α and x ∈ β, ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ.

Русский

Для всех r ∈ α и x ∈ β выполняется ‖r • x‖ₑ = ‖r‖ₑ · ‖x‖ₑ.

LaTeX

$$$‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ$$

Lean4

theorem enorm_smul [ENorm α] [ENorm β] [SMul α β] [ENormSMulClass α β] (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ :=
  ENormSMulClass.enorm_smul r x

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

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

Разделы

Аффилиация

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