mul — Mathlib

English

If f and g are LipschitzWith with constants Kf, Kg, then the product x ↦ f(x) g(x) is LipschitzWith with constant Kf+Kg.

Русский

Если f и g липшицевы с константами Kf и Kg, то произведение x↦f(x)g(x) липшицево с константой Kf+Kg.

LaTeX

$$$\\mathrm{LipschitzWith}\\ K_f f \\land \\mathrm{LipschitzWith}\\ Kg\\ g \\Rightarrow \\mathrm{LipschitzWith}\\ (K_f+K_g)\\ (\\lambda x. f(x)g(x)).$$$

Lean4

@[to_additive]
theorem mul (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun x ↦ f x * g x := by
  simpa [← lipschitzOnWith_univ] using hf.lipschitzOnWith.mul hg.lipschitzOnWith

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