English
Let f be a family of uniformly Lipschitz functions f: γ → α →ᵤ β with a common Lipschitz constant K on a set s ⊆ γ. Then f is Lipschitz on s if and only if every coordinate function x ↦ (f(x))(c) is Lipschitz on s for all c ∈ α.
Русский
Пусть f: γ → α →ᵤ β задаёт семейство функций с общей константой Липшица K на множества s ⊆ γ. Тогда f липшицева на s тогда и только тогда, когда для каждого координатного слагаемого c ∈ α функция x ↦ (f(x))(c) тоже липшицева на s.
LaTeX
$$$\mathrm{LipschitzOnWith} K f s \;\Longleftrightarrow\; \forall c,\; \mathrm{LipschitzOnWith} K\big(\lambda x. (f\,x)(c)\big) s$$$
Lean4
theorem lipschitzOnWith_iff {f : γ → α →ᵤ β} {K : ℝ≥0} {s : Set γ} :
LipschitzOnWith K f s ↔ ∀ c, LipschitzOnWith K (fun x ↦ toFun (f x) c) s :=
by
simp [lipschitzOnWith_iff_restrict, lipschitzWith_iff]
rfl
