English
If f and g are analytic on nhd(s) and g(x) ≠ 0 for x ∈ s, then f/g is analytic on nhd(s).
Русский
Если f и g аналитичны на окрестности s и g(x) ≠ 0 для x ∈ s, то f/g аналитично на окрестности s.
LaTeX
$$$\\mathit{AnalyticOnNhd}_{\\mathfrak k}(f,s) \\wedge \\mathit{AnalyticOnNhd}_{\\mathfrak k}(g,s) \\wedge \\forall x \\in s,\, g(x) \\neq 0 \\Rightarrow \\mathit{AnalyticOnNhd}_{\\mathfrak k}(\\lambda t. f(t)/g(t), s).$$$
Lean4
/-- `f x / g x` is analytic away from `g x = 0` -/
theorem div {f g : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s) (ga : AnalyticOnNhd 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) :
AnalyticOnNhd 𝕜 (fun x ↦ f x / g x) s := fun x m ↦ (fa x m).div (ga x m) (g0 x m)
