lipschitzWith_smul

Mathlib.Analysis.Normed.MulAction

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

English

The map x ↦ s • x is Lipschitz with constant ‖s‖₊ in β.

Русский

Отображение x ↦ s • x является липшицевым с константой ‖s‖₊ на β.

LaTeX

$$$\\mathrm{LipschitzWith}\\left(\\|s\\|_+\\right)\\left(\\,\\cdot \\mapsto s \\cdot \\cdot\\right)$$$

Lean4

theorem lipschitzWith_smul (s : α) : LipschitzWith ‖s‖₊ (s • · : β → β) :=
  lipschitzWith_iff_dist_le_mul.2 <| dist_smul_le _

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

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

Разделы

Аффилиация

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