div — Mathlib

English

If f and g are globally continuous and g(x) ≠ 0 for all x, then the quotient f/g is continuous.

Русский

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

LaTeX

$$Continuous f → Continuous g → (∀ x, Ne (g x) 0) → Continuous (\\lambda x, f(x) / g(x))$$

Lean4

@[continuity]
theorem div (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) : Continuous (f / g) := by
  simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

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