edist_le

Mathlib.Topology.MetricSpace.UniformConvergence

URI: https://scilib.ai/kg/mathlib#UniformFun.edist_le

English

edist(f,g) ≤ C if and only if for all x, edist(f(x),g(x)) ≤ C.

Русский

edist(f,g) ≤ C тогда и только тогда, когда для всех x выполняется edist(f(x),g(x)) ≤ C.

LaTeX

$$edist(f,g) ≤ C \iff \forall x, edist(f(x),g(x)) ≤ C$$

Lean4

theorem edist_le {f g : α →ᵤ β} {C : ℝ≥0∞} : edist f g ≤ C ↔ ∀ x, edist (toFun f x) (toFun g x) ≤ C :=
  iSup_le_iff

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

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

Разделы

Аффилиация

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