bound_of_antilipschitz

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

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

← MathLib Explorer

English

If a linear map is antilipschitz with constant K, then ∥x∥ ≤ K ∥f x∥.

Русский

Если линейная карта антизлипшит с константой K, то ∥x∥ ≤ K ∥f x∥.

LaTeX

$$$\text{AntilipschitzWith } K f \Rightarrow \|x\| ≤ K \|f x\|$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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