Proposition to_way_below_prod {xy₁ xy₂ : prod_dcpo X Y} (p : pr1 xy₁ ≪ pr1 xy₂) (q : pr2 xy₁ ≪ pr2 xy₂) : xy₁ ≪ xy₂. Proof. intros D r. rewrite prod_dcpo_lub in r. assert (H := p (directed_set_comp π₁ D) (pr1 r)). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ i s₁ ]. assert (H := q (directed_set_comp π₂ D) (pr2 r)). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ j s₂ ]. assert (H := directed_set_top D i j). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ t [ u₁ u₂ ]]. simple refine (hinhpr (t ,, _ ,, _)). - exact (trans_dcpo s₁ (pr1 u₁)). - exact (trans_dcpo s₂ (pr2 u₂)). Qed.
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.