nndist_le_two_nnnorm

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.nndist_le_two_nnnorm

English

For x,y ∈ α, the nonnegative distance between f x and f y is bounded by 2 times the NN-norm of f: nndist (f x) (f y) ≤ 2 * ‖f‖₊.

Русский

Для x,y∈α расстояние между f(x) и f(y) в NNNorm ограничено: nndist (f x) (f y) ≤ 2 · ‖f‖₊.

LaTeX

$$$\mathrm{nndist}(f(x), f(y)) \leq 2 \|f\|_+$$$

Lean4

theorem nndist_le_two_nnnorm (x y : α) : nndist (f x) (f y) ≤ 2 * ‖f‖₊ :=
  dist_le_two_norm _ _ _

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

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

Разделы

Аффилиация

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