prodMk — Mathlib

English

If f and g are continuous at x, then the map x ↦ (f x, g x) is continuous at x.

Русский

Если f и g непрерывны в точке x, то отображение x ↦ (f(x), g(x)) непрерывно в x.

LaTeX

$$$ \\text{ContinuousAt } f x \\; \\land \\; \\text{ContinuousAt } g x \\Rightarrow \\text{ContinuousAt } (\\\\lambda x. (f x, g x)) x $$$

Lean4

@[fun_prop]
theorem prodMk {f : X → Y} {g : X → Z} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
    ContinuousAt (fun x => (f x, g x)) x :=
  hf.prodMk_nhds hg

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