proposition: Proposition to_way_below_prod {xy₁ xy₂ : prod_dcpo X Y} (p : pr1 xy₁ ≪ pr1 xy₂) (q : pr2 xy₁ ≪ pr2 xy₂) : xy₁ ≪ xy₂.
proof: 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.
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