div — Mathlib

English

If f and g are continuous on s and g(x) ≠ 0 for all x ∈ s, then f/g is continuous on s.

Русский

Если f и g непрерывны на s и для всех x ∈ s выполняется g(x) ≠ 0, то f/g непрерывна на s.

LaTeX

$$ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → ContinuousOn (\\lambda x, f(x) / g(x)) s$$

Lean4

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

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