prodMk — Mathlib

English

If f is continuous within s at x and g is continuous within t at y, then the map (f,g) into the product is continuous within s×t at (x,y).

Русский

Если f непрерывна внутри s в x и g непрерывна внутри t в y, то Prod.map f g непрерывна внутри s×t в (x,y).

LaTeX

$$$\text{ContinuousWithinAt } f\ s\ x \to \text{ContinuousWithinAt } g\ t\ y \to \text{ContinuousWithinAt } (Prod.map f g) \ (s \times\{t\})\ (x,y)$$$

Lean4

@[fun_prop]
theorem prodMk {f : α → β} {g : α → γ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x => (f x, g x)) s := fun x hx => (hf x hx).prodMk (hg x hx)

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