proposition: Proposition prod_is_scott_open (PA : scott_open_set A) (PB : scott_open_set B) : is_scott_open (λ (x : (A × B)%dcpo), PA (pr1 x) ∧ PB (pr2 x)).
proof: Proof. split. - intros ( a₁ & b₁ ) ( a₂ & b₂ ) ( p₁ & p₂ ) ( q₁ & q₂ ). exact (is_scott_open_upper_set PA p₁ q₁ ,, is_scott_open_upper_set PB p₂ q₂). - intros D ( p & q ). rewrite prod_dcpo_lub in p, q. cbn in p, q. assert (H₁ := is_scott_open_lub_inaccessible PA (directed_set_comp π₁ D) p). assert (H₂ := is_scott_open_lub_inaccessible PB (directed_set_comp π₂ D) q). revert H₁. use factor_through_squash_hProp. intros ( i₁ & H₁ ) ; cbn in i₁, H₁. revert H₂. use factor_through_squash_hProp. intros ( i₂ & H₂ ) ; cbn in i₂, H₂. assert (H₃ := directed_set_top D i₁ i₂). revert H₃. use factor_through_squash_hProp. intros ( k & r₁ & r₂ ) ; cbn in k, r₁, r₂. refine (hinhpr (k ,, _ ,, _)). + exact (is_scott_open_upper_set PA H₁ (pr1 r₁)). + exact (is_scott_open_upper_set PB H₂ (pr2 r₂)). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal