div — Mathlib

English

If hf : LocallyLipschitzOn s f and hg : LocallyLipschitzOn s g, then the division f(x)/g(x) is LocallyLipschitzOn on s.

Русский

Если hf и hg — локально липшицевы на s, то f(x)/g(x) локально липшицево на s.

LaTeX

$$$\\mathrm{LocallyLipschitzOn}\\ s\\ f \\land \\mathrm{LocallyLipschitzOn}\\ s\\ g \\Rightarrow \\mathrm{LocallyLipschitzOn}\\ s\\ (\\lambda x. f(x)/g(x)).$$$

Lean4

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

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