div — Mathlib

English

If hf : LipschitzOnWith Kf f s and hg : LipschitzOnWith Kg g s, then the product is LipschitzOnWith with constant Kf+Kg on s.

Русский

Если hf и hg — липшицевы на s с константами Kf и Kg, то произведение f g — липшицево на s с константой Kf+Kg.

LaTeX

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

Lean4

@[to_additive]
theorem div (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
    LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s := by simpa only [div_eq_mul_inv] using hf.mul hg.inv

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