LipschitzOnWith — Mathlib

English

If s ⊆ t then diam s ≤ diam t.

Русский

Если s ⊆ t, то диаметр s не больше диаметра t.

LaTeX

$$\operatorname{diam}(s) \le \operatorname{diam}(t) \quad (s \subseteq t)$$

Lean4

/-- A function `f` is **Lipschitz continuous** with constant `K ≥ 0` **on `s`** if
for all `x, y` in `s` we have `dist (f x) (f y) ≤ K * dist x y`. -/
def LipschitzOnWith (K : ℝ≥0) (f : α → β) (s : Set α) :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → edist (f x) (f y) ≤ K * edist x y

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