antilipschitz

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

← MathLib Explorer

English

A semilinear isometry is antilipschitz with constant 1.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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