div' — Mathlib

English

If f and g are continuous, then the map x ↦ f(x)/g(x) is continuous.

Русский

Если f и g непрерывны, то отображение x ↦ f(x)/g(x) непрерывно.

LaTeX

$$$\\mathrm{Continuous}(f) \\land \\mathrm{Continuous}(g) \\Rightarrow \\mathrm{Continuous}\\bigl(x \\mapsto f(x)/g(x)\\bigr)$$$

Lean4

@[to_additive (attr := continuity, fun_prop) sub]
theorem div' (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x / g x :=
  continuous_div'.comp₂ hf hg

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