lipschitz

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#SemilinearIsometryClass.lipschitz

English

A semilinear isometry is Lipschitz with constant 1.

Русский

Семилинейная изометрия липшицево ограничена константой 1.

LaTeX

$$$\operatorname{LipschitzWith}(1,f)$$$

Lean4

protected theorem lipschitz [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : LipschitzWith 1 f :=
  (SemilinearIsometryClass.isometry f).lipschitz

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

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

Разделы

Аффилиация

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