div — Mathlib

English

If hf : LocallyLipschitz f and hg : LocallyLipschitz g, then the division f/g is LocallyLipschitz.

Русский

Если f и g локально липшицевы, то f/g локально липшицево.

LaTeX

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

Lean4

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

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