div — Mathlib

English

Same as above: 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}(\lambda t. f(t)/g(t))(x).$$$

Lean4

@[fun_prop]
theorem div {f g : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
    AnalyticAt 𝕜 (f / g) x :=
  fa.fun_div ga g0

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