comp_sub — Mathlib

English

If f is analytic within s at x, then z ↦ f(z−y) is analytic within s+{y} at x+y.

Русский

Если f аналитична внутри s в точке x, то z↦f(z−y) аналитична внутри s+{y} в точке x+y.

LaTeX

$$$AnalyticWithinAt\ 𝕜\ f\ s\ x \Rightarrow \forall y,\ AnalyticWithinAt\ 𝕜\ (\\fun z \\to f (z - y))\ (s + { y })\ (x + y)$$$

Lean4

theorem comp_sub (hf : AnalyticWithinAt 𝕜 f s x) (y : E) : AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + { y }) (x + y) :=
  by
  obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

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