prod — Mathlib

English

The Cartesian product of analytic functions is analytic.

Русский

Картезианово произведение аналитических функций аналитично.

LaTeX

$$$(\\text{AnalyticOnNhd 𝕜 f s}) \\land (\\text{AnalyticOnNhd 𝕜 g s}) \\Rightarrow (\\text{AnalyticOnNhd 𝕜} (fun x \\mapsto (f x, g x)) s)$$$

Lean4

/-- The Cartesian product of analytic functions is analytic. -/
theorem prod {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
    AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s := fun x hx ↦ (hf x hx).prod (hg x hx)

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