div' — Mathlib

English

If f and g are ContinuousWithinAt on s at x, then f/g is ContinuousWithinAt on s at x.

Русский

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

LaTeX

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

Lean4

@[to_additive sub]
theorem div' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
    ContinuousWithinAt (fun x => f x / g x) s x :=
  Filter.Tendsto.div' hf hg

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