Scott continuity on product spaces

Main result

• ScottContinuous_prod_of_ScottContinuous: A function is Scott continuous on a product space if it is Scott continuous in each variable.
• ScottContinuousOn.inf₂: For complete linear orders, the meet operation is Scott continuous.

theorem ScottContinuousOn.fromProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {f : α × β → γ} {D : Set (Set (α × β))} (h₁ : ∀ (a : α), ScottContinuousOn ((fun (d : Set (α × β)) => Prod.snd '' d) '' D) fun (b : β) => f (a, b)) (h₂ : ∀ (b : β), ScottContinuousOn ((fun (d : Set (α × β)) => Prod.fst '' d) '' D) fun (a : α) => f (a, b)) (h₁' : ∀ (a : α), Monotone fun (b : β) => f (a, b)) (h₂' : ∀ (b : β), Monotone fun (a : α) => f (a, b)) : ScottContinuousOn D f

If is Scott continuous on a product space if it is Scott continuous and monotone in each variable

theorem ScottContinuous.fromProd {α : Type u_1} {β : Type u_2} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {f : α × β → γ} (h₁ : ∀ (a : α), ScottContinuous fun (b : β) => f (a, b)) (h₂ : ∀ (b : β), ScottContinuous fun (a : α) => f (a, b)) : ScottContinuous f

theorem ScottContinuous.prod {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} [Preorder α] [Preorder β] [Preorder α'] [Preorder β'] {f : α → α'} {g : β → β'} (hf : ScottContinuous f) (hg : ScottContinuous g) : ScottContinuous (Prod.map f g)