nndist_le_opNNNorm

Mathlib.Analysis.Normed.Operator.NNNorm

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

English

The distance between f x and f y is bounded by the operator norm of f times the distance between x and y.

Русский

Расстояние между f x и f y не превосходит ‖f‖₊ · dist(x,y).

LaTeX

$$$nndist\\big(f x, f y\\big) \\le \\|f\\|_{+} \\cdot nndist(x,y)$$$

Lean4

theorem nndist_le_opNNNorm (f : E →SL[σ₁₂] F) (x y : E) : nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y :=
  dist_le_opNorm f x y

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

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

Разделы

Аффилиация

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