restrict — Mathlib

English

The restriction of a K-Lipschitz function to a subset is K-Lipschitz.

Русский

Ограничение K‑липшицева функция на подмножество сохраняет константу липшицевости.

LaTeX

$$$\\text{LipschitzWith } K f \\Rightarrow \\text{ LipschitzWith } K (s.restrict f)$$$

Lean4

/-- The restriction of a `K`-Lipschitz function is `K`-Lipschitz. -/
protected theorem restrict (hf : LipschitzWith K f) (s : Set α) : LipschitzWith K (s.restrict f) := fun x y => hf x y

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