lipschitzOnWith_ofFun_iff — Mathlib

English

Let f: γ → α → β be a family of functions. The map x ↦ ofFun(f(x)) is Lipschitz with constant K on s iff each coordinate map c ↦ f(x)·c is Lipschitz with the same constant on s for all c.

Русский

Пусть f: γ → α → β задаёт семейство функций. Отображение x ↦ ofFun(f(x)) липшицево на s с константой K тогда и только тогда, когда для каждого координатного c константа Lip остаётся K для функции x ↦ f(x)·c.

LaTeX

$$$\mathrm{LipschitzOnWith} K (\lambda x. \mathrm{ofFun}(f x)) s \;\Longleftrightarrow\; \forall c,\; \mathrm{LipschitzOnWith} K (f \cdot c) s$$$

Lean4

theorem lipschitzOnWith_ofFun_iff {f : γ → α → β} {K : ℝ≥0} {s : Set γ} :
    LipschitzOnWith K (fun x ↦ ofFun (f x)) s ↔ ∀ c, LipschitzOnWith K (f · c) s :=
  lipschitzOnWith_iff

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