mul — Mathlib

English

If f and g are locally Lipschitz, then the product x ↦ f(x) g(x) is locally Lipschitz.

Русский

Если f и g локальноLipшицевы, то произведение f(x)g(x) локально липшицево.

LaTeX

$$$\\mathrm{LocallyLipschitz} f \\land \\mathrm{LocallyLipschitz} g \\Rightarrow \\mathrm{LocallyLipschitz} (\\lambda x. f(x)g(x)).$$$

Lean4

@[to_additive]
theorem mul (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun x ↦ f x * g x := by
  simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn

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