antilipschitz_of_bound

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.antilipschitz_of_bound

← MathLib Explorer

English

A bound of the form ∥x∥ ≤ K ∥f x∥ implies antilipschitzness with constant K.

Русский

Неравенство нормы задаёт антипсилос с константой K.

LaTeX

$$$\text{AntilipschitzWith } K\ f$ given $\forall x, \|x\| ≤ K \|f x\|$$$

Lean4

theorem antilipschitz_of_bound (f : E →SL[σ] F) {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f :=
  AddMonoidHomClass.antilipschitz_of_bound _ h

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

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

Разделы

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

Аффилиация

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