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))
:
If is Scott continuous on a product space if it is Scott continuous and monotone in each variable
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)