div' — Mathlib

English

If f and g are ContinuousOn on s, then f/g is ContinuousOn on s.

Русский

Если f и g непрерывны на s, то f/g непрерывна на s.

LaTeX

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

Lean4

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

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