div₀ — Mathlib

English

The quotient of two continuous-at functions is continuous at a when the denominator is nonzero at that point.

Русский

Частное двух функций, непрерывных в точке, непрерывно в этой точке, если знаменатель не равен нулю в этой точке.

LaTeX

$$theorem div₀ (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) : ContinuousAt (\\lambda x, f x / g x) a$$

Lean4

@[fun_prop]
theorem div₀ (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
    ContinuousOn (fun x => f x / g x) s :=
  ContinuousOn.div hf hg h₀

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