English
If f and g are analytic within a set s at x, and g(x) ≠ 0, then f/g is analytic within s at x.
Русский
Если f и g аналитичны на внутреннем со множестве s в точке x и g(x) ≠ 0, то f(x)/g(x) аналитично на s в x.
LaTeX
$$$\mathit{AnalyticWithinAt}_{\mathfrak k}(f,s,x) \wedge \mathit{AnalyticWithinAt}_{\mathfrak k}(g,s,x) \wedge g(x) \neq 0 \Rightarrow \mathit{AnalyticWithinAt}_{\mathfrak k}\bigl(\lambda t. f(t)/g(t)\bigr)(s,x).$$$
Lean4
/-- `f x / g x` is analytic away from `g x = 0` -/
theorem div {f g : E → 𝕝} {s : Set E} {x : E} (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x)
(g0 : g x ≠ 0) : AnalyticWithinAt 𝕜 (fun x ↦ f x / g x) s x := by simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0)
