smul_congr

Mathlib.Analysis.LocallyConvex.Basic

URI: https://scilib.ai/kg/mathlib#Balanced.smul_congr

English

If hs is balanced and ‖a‖ = ‖b‖, then a · s = b · s.

Русский

Если s сбалансировано и ‖a‖ = ‖b‖, то a · s = b · s.

LaTeX

$$$\\text{Balanced } 𝕝 \\land \\|a\\| = \\|b\\| \\Rightarrow a \\cdot s = b \\cdot s$$$

Lean4

theorem smul_congr (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • s = b • s :=
  (hs.smul_mono h.le).antisymm (hs.smul_mono h.ge)

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

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

Разделы

Аффилиация

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