mk_one — Mathlib

English

A one-Lipschitz condition can be constructed from pointwise distance inequalities on a set.

Русский

Из неравенств на расстоянии можно построить одно-липшицево условие.

LaTeX

$$$\\operatorname{LipschitzOnWith}(1, f, s)$ given $\\forall x,y\\in s:\\; d(f(x),f(y)) ≤ d(x,y)$$$

Lean4

protected theorem mk_one (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) : LipschitzOnWith 1 f s :=
  of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h

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