English
If f,g are Scott-continuous, then their Prod.map is Scott-continuous: (f,g) ↦ Prod.map f g is Scott-continuous.
Русский
Если f,gScott–непрерывны, то отображение Prod.map f g Scott–непрерывно.
LaTeX
$$$\\mathrm{ScottContinuous}(f) \\to \\mathrm{ScottContinuous}(g) \\to \\mathrm{ScottContinuous}(\\mathrm{Prod.map}\\ f\\ g).$$$
Lean4
theorem prod {α' β' : Type*} [Preorder α] [Preorder β] [Preorder α'] [Preorder β'] {f : α → α'} {g : β → β'}
(hf : ScottContinuous f) (hg : ScottContinuous g) : ScottContinuous (Prod.map f g) :=
by
refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)
· have e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d) := by aesop
simp_rw [Prod.map_apply, e1]
exact .prod (singleton_nonempty _) (hd₁.image _) isLUB_singleton (hg hd₁ hd₂ hdc)
· have e2 : ((fun a ↦ (f a, g b)) '' d) = (f '' d) ×ˢ {g b} := by aesop
simp_rw [Prod.map_apply, e2]
exact .prod (hd₁.image _) (singleton_nonempty _) (hf hd₁ hd₂ hdc) isLUB_singleton
