dist_coe_le_dist — Mathlib

English

For every x, the pointwise distance is at most the uniform distance dist f g.

Русский

Для каждого x выполняется dist(f(x), g(x)) ≤ dist(f,g).

LaTeX

$$$\forall x:\alpha, \operatorname{dist}(f(x), g(x)) \le \operatorname{dist}(f,g)$$$

Lean4

/-- The pointwise distance is controlled by the distance between functions, by definition. -/
theorem dist_coe_le_dist (x : α) : dist (f x) (g x) ≤ dist f g :=
  le_csInf dist_set_exists fun _ hb => hb.2 x

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