dist_le

Mathlib.Topology.MetricSpace.Holder

URI: https://scilib.ai/kg/mathlib#HolderWith.dist_le

English

HolderWith implies a bound on the distance after applying f, for all x,y.

Русский

HolderWith обеспечивает неравенство на расстояние после применения f для произвольных x,y.

LaTeX

$$$\operatorname{dist}(f(x), f(y)) \le C \cdot \operatorname{dist}(x,y)^{r}$$$

Lean4

theorem dist_le (hf : HolderWith C r f) (x y : X) : dist (f x) (f y) ≤ C * dist x y ^ (r : ℝ) :=
  hf.dist_le_of_le le_rfl

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

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

Разделы

Аффилиация

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