sigmoid — Mathlib

English

If f is analytic on a neighborhood of a set s, then sigmoid ∘ f is analytic on that neighborhood of s.

Русский

Если f аналитична в окрестности множества s, то sigmoid ∘ f аналитична в той же окрестности.

LaTeX

$$$\mathrm{AnalyticOnNhd}_{\mathbb{R}} (f, s) \Rightarrow \mathrm{AnalyticOnNhd}_{\mathbb{R}} (\operatorname{sigmoid} \circ f, s)$$$

Lean4

theorem sigmoid (fs : AnalyticOnNhd ℝ f s) : AnalyticOnNhd ℝ (sigmoid ∘ f) s := fun z n ↦
  analyticAt_sigmoid.comp (fs z n)

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