comp_sub — Mathlib

English

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

Русский

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

LaTeX

$$$AnalyticAt\ 𝕜\ f\ x \Rightarrow \forall y,\ AnalyticAt\ 𝕜\ (\\fun z \\to f (z - y))\ (x + y)$$$

Lean4

theorem comp_sub (hf : AnalyticOnNhd 𝕜 f s) (y : E) : AnalyticOnNhd 𝕜 (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

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