comp_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_sub (hf : AnalyticOn 𝕜 f s) (y : E) : AnalyticOn 𝕜 (fun z ↦ f (z - y)) (s + { y }) :=
  by
  intro x hx
  simp only [add_singleton, image_add_right, mem_preimage] at hx
  rw [show x = (x - y) + y by abel]
  apply (hf (x - y) (by convert hx using 1; abel)).comp_sub

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