Definition dcpo_continuous_struct_product {X Y : dcpo} (CX : continuous_dcpo_struct X) (CY : continuous_dcpo_struct Y) : continuous_dcpo_struct (prod_dcpo X Y). Proof. use continuous_struct_from_basis. use prod_dcpo_basis. - use basis_from_continuous_struct. exact CX. - use basis_from_continuous_struct. exact CY. Defined.
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.