English
Scott-continuity in each coordinate implies Scott-continuity of the product map: if f,g are Scott-continuous on D, then x ↦ (f x, g x) is Scott-continuous on D.
Русский
Скоттовская непрерывность по каждой координате влечет за собой непрерывность произведения: если f,g Scott–непрерывны на D, то x ↦ (f x, g x) Scott–непрерывна на D.
LaTeX
$$$(\\forall a, \\mathrm{ScottContinuousOn}\, D\\,(f), )$$$
Lean4
theorem fromProd {γ : Type*} [Preorder α] [Preorder β] [Preorder γ] {f : α × β → γ}
(h₁ : ∀ a, ScottContinuous (fun b => f (a, b))) (h₂ : ∀ b, ScottContinuous (fun a => f (a, b))) :
ScottContinuous f := by
simp_rw [← scottContinuousOn_univ] at ⊢
exact
.fromProd (fun a ↦ (h₁ a).scottContinuousOn) (fun b ↦ (h₂ b).scottContinuousOn) (fun a ↦ (h₁ a).monotone)
(fun b ↦ (h₂ b).monotone)
