prodMk — Mathlib

English

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

Русский

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

LaTeX

$$$\text{ContinuousWithinAt } f\ s\ x \to \text{ContinuousWithinAt } g\ s\ x \to \text{ContinuousWithinAt } (\lambda x. (f x, g x))\ s\ x$$$

Lean4

theorem prodMk {f : α → β} {g : α → γ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x)
    (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun x => (f x, g x)) s x :=
  hf.prodMk_nhds hg

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