Slices of analytic functions of two variables

Mathlib's AnalyticAt.curry_right says that a function analytic at p on a product has an analytic slice y ↦ f (p.1, y) at p.2. Since the analytic locus is open, the same holds for the slices y ↦ f (x, y) with x near p.1 (AnalyticAt.eventually_analyticAt_curry_right).

theorem AnalyticAt.eventually_analyticAt_curry_right {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E × E' → F} {p : E × E'} (hf : AnalyticAt 𝕜 f p) : ∀ᶠ (x : E) in nhds p.1, AnalyticAt 𝕜 (fun (y : E') => f (x, y)) p.2

The slices y ↦ f (x, y) of a function analytic at p are analytic at p.2 for every x near p.1.