abs_diff_coe_le_dist

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

For bounded continuous f,g, the pointwise difference is bounded by the distance between f and g.

Русский

Для f,g: α →ᵇ β, предел по x: ‖f(x) − g(x)‖ ≤ dist(f,g).

LaTeX

$$$‖f x - g x‖ ≤ dist f g$$$

Lean4

theorem abs_diff_coe_le_dist : ‖f x - g x‖ ≤ dist f g :=
  by
  rw [dist_eq_norm]
  exact (f - g).norm_coe_le_norm x

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

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

Разделы

Аффилиация

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