Definition tensor_scott_continuous_map {X₁ X₂ Y₁ Y₂ : dcpo} (f₁ : scott_continuous_map X₁ Y₁) (f₂ : scott_continuous_map X₂ Y₂) : scott_continuous_map (X₁ × X₂) (Y₁ × Y₂) := ⟨ π₁ · f₁ , π₂ · f₂ ⟩.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.