div — Mathlib

English

If f and g are continuous at a and g(a) ≠ 0, then f/g is continuous at a.

Русский

Если f и g непрерывны в точке a и g(a) ≠ 0, то f(a)/g(a) непрерывно в a.

LaTeX

$$ContinuousAt f a → ContinuousAt g a → Ne (g a) 0 → ContinuousAt (\\lambda x, f(x) / g(x)) a$$

Lean4

/-- Continuity at a point of the result of dividing two functions continuous at that point, where
the denominator is nonzero. -/
nonrec theorem div (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (f / g) a :=
  hf.div hg h₀

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