prodMap — Mathlib

English

If f is continuous on s and g is continuous on t, then Prod.map f g is continuous on s × t.

Русский

Если f непрерывна на s, а g непрерывна на t, тогда Prod.map f g непрерывна на s × t.

LaTeX

$$$\text{ContinuousOn } f\ s \to \text{ContinuousOn } g\ t \to \text{ContinuousOn } (Prod.map f g) (s \times^\! t)$$$

Lean4

theorem prodMap {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) :
    ContinuousOn (Prod.map f g) (s ×ˢ t) := fun ⟨x, y⟩ ⟨hx, hy⟩ => (hf x hx).prodMap (hg y hy)

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