prod — Mathlib

English

Let f: E → F and g: E → G be analytic on a set s ⊆ E. Then the map x ↦ (f(x), g(x)) is analytic on s.

Русский

Пусть f: E → F и g: E → G аналитичны на множества s ⊆ E. Тогда отображение x ↦ (f(x), g(x)) аналитично на s.

LaTeX

$$$\\forall f:E\\to F\\,\\forall g:E\\to G\\,\\forall s\\subseteq E,\\; (AnalyticOn 𝕜 f s) \\land (AnalyticOn 𝕜 g s) \\Rightarrow AnalyticOn 𝕜 (fun x \\mapsto (f x, g x)) s$$$

Lean4

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

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