nnnorm_smul

Mathlib.Analysis.Normed.MulAction

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

English

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

Русский

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

LaTeX

$$$‖r • x‖₊ = ‖r‖₊ * ‖x‖₊$$

Lean4

theorem nnnorm_smul (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ :=
  NNReal.eq <| norm_smul r x

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

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

Разделы

Аффилиация

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