fun_div — Mathlib

English

If f and g are analytic at x and g(x) ≠ 0, then f/g is analytic at x.

Русский

Если f и g аналитичны в точке x и g(x) ≠ 0, то f/g аналитично в x.

LaTeX

$$$\mathit{AnalyticAt}_{\mathfrak k}(f,x) \wedge \mathit{AnalyticAt}_{\mathfrak k}(g,x) \wedge g(x) \neq 0 \Rightarrow \mathit{AnalyticAt}_{\mathfrak k}\bigl(\lambda t. f(t)/g(t)\bigr)(x).$$$

Lean4

/-- `f x / g x` is analytic away from `g x = 0` -/
@[fun_prop]
theorem fun_div {f g : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
    AnalyticAt 𝕜 (fun x ↦ f x / g x) x := by simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0)

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