div' — Mathlib

English

If f and g are continuous at a point x, then f/g is continuous at x.

Русский

Если функции f и g непрерывны в точке x, то f/g непрерывна в x.

LaTeX

$$$\\mathrm{ContinuousAt}(f,x) \\Rightarrow \\mathrm{ContinuousAt}(g,x) \\Rightarrow \\mathrm{ContinuousAt}\\bigl(x \\mapsto f(x)/g(x)\\bigr) x$$$

Lean4

@[to_additive (attr := fun_prop) sub]
nonrec theorem div' (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x => f x / g x) x :=
  hf.div' hg

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