English
If f maps x to y and g is analytic at y, f is analytic at x, and mapsTo holds, then comp g f is analytic at x; i.e., comp_of_eq.
Русский
Если f переводит x в y, а g аналитична в y, и выполняется отображение, то композиция g∘f аналитична в x.
LaTeX
$$$\\text{AnalyticWithinAt } (g\\circ f)\\; x = \\text{AnalyticWithinAt } g\\; (f x) \\quad \\text{ under assumptions } hg, hf, h, hy$.$$
Lean4
/-- Version of `AnalyticWithinAt.comp` where point equality is a separate hypothesis. -/
theorem comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} {t : Set F} {s : Set E} (hg : AnalyticWithinAt 𝕜 g t y)
(hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t) (hy : f x = y) : AnalyticWithinAt 𝕜 (g ∘ f) s x :=
by
rw [← hy] at hg
exact hg.comp hf h
