div — Mathlib

English

If f and g are analytic on s and g never vanishes on s, then the quotient x ↦ f(x)/g(x) is analytic on s.

Русский

Пусть f и g аналитичны на s и ∀z∈s, g(z) ≠ 0. Тогда x ↦ f(x)/g(x) аналитична на s.

LaTeX

$$$\\text{If } f,g:E\\to 𝕝 \\text{ are AnalyticOn 𝕜 on } s, \\text{ and } ∀x∈s,\ g(x) \\neq 0, \\text{ then } x\\mapsto f(x)/g(x) \\text{ is AnalyticOn 𝕜 on } s.$$$

Lean4

/-- `f x / g x` is analytic away from `g x = 0` -/
theorem div {f g : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
    AnalyticOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦ (fa x m).div (ga x m) (g0 x m)

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