coe_le_coe_add_dist

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

For real-valued bounded maps f,g, the pointwise value satisfies f(x) ≤ g(x) + dist(f,g).

Русский

Для f,g: α →ᵇ ℝ выполнено f(x) ≤ g(x) + dist(f,g) для каждого x.

LaTeX

$$$f x \\le g x + dist f g$$$

Lean4

theorem coe_le_coe_add_dist {f g : α →ᵇ ℝ} : f x ≤ g x + dist f g :=
  sub_le_iff_le_add'.1 <| (abs_le.1 <| @dist_coe_le_dist _ _ _ _ f g x).2

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

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

Разделы

Аффилиация

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