comp' — Mathlib

English

If two maps g and f are analytic respectively at f(x) and x, then the composed map g ∘ f is analytic at x, written with the prime version.

Русский

Если функции g и f аналитичны в точках f(x) и x соответственно, то их композиция g ∘ f аналитична в x (вариант с апострофом).

LaTeX

$$$AnalyticAt 𝕜 g (f x) \\land AnalyticAt 𝕜 f x \\Rightarrow AnalyticAt 𝕜 (fun z \\mapsto g (f z)) x$$$

Lean4

/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is
analytic at `x`. -/
@[fun_prop]
theorem comp' {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) :
    AnalyticAt 𝕜 (fun z ↦ g (f z)) x :=
  hg.comp hf

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