prod — Mathlib

English

The cartesian product of analytic functions at a point is analytic at that point.

Русский

Карточная пара аналитичных функций в точке аналитична в этой точке.

LaTeX

$$$\text{AnalyticAt}(f, x) \land \text{AnalyticAt}(g, x) \Rightarrow \text{AnalyticAt}(x \mapsto (f(x), g(x)), x)$$$

Lean4

/-- The Cartesian product of analytic functions is analytic. -/
@[fun_prop]
theorem prod {e : E} {f : E → F} {g : E → G} (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) :
    AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e := by
  rcases hf with ⟨_, hf⟩
  rcases hg with ⟨_, hg⟩
  exact ⟨_, hf.prod hg⟩

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