nndist_coe_le_nndist — Mathlib

English

Let f,g : α →ᵇ β be bounded continuous functions. For every x ∈ α, the distance in β between f(x) and g(x) is bounded above by the distance in the function space: nndist (f x) (g x) ≤ nndist f g.

Русский

Пусть f,g : α →ᵇ β — ограниченные непрерывные функции. Для каждого x ∈ α выполняется неотрицательная верхняя оценка: nndist (f x) (g x) ≤ nndist f g.

LaTeX

$$$\\forall x \\in \\alpha,\\; \\operatorname{nndist}(f(x), g(x)) \\le \\operatorname{nndist}(f, g).$$$

Lean4

theorem nndist_coe_le_nndist (x : α) : nndist (f x) (g x) ≤ nndist f g :=
  dist_coe_le_dist x

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