nndist_set_exists

Mathlib.Topology.ContinuousMap.Bounded.Basic

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

English

There exists a nonnegative C such that ∀ x, nndist(f x) (g x) ≤ C.

Русский

Существует неотрицательное C такое, что для всех x выполняется nndist(f(x), g(x)) ≤ C.

LaTeX

$$$\exists C, ∀ x:\alpha, nndist (f x) (g x) \le C$$$

Lean4

theorem nndist_set_exists : ∃ C, ∀ x : α, nndist (f x) (g x) ≤ C :=
  Subtype.exists.mpr <| dist_set_exists.imp fun _ ⟨ha, h⟩ => ⟨ha, h⟩

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

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

Разделы

Аффилиация

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