proposition: Proposition continuous_dcpo_struct_way_below (x y : X) : x ≪ y ≃ ∃ (i : approximating_family CX y), x ⊑ approximating_family CX y i.
proof: Proof. use weqimplimpl. - intro p. apply (p (approximating_family CX y)). rewrite approximating_family_lub. apply refl_dcpo. - use factor_through_squash. { apply propproperty. } intro H. induction H as [ i p ]. refine (trans_le_way_below p _). apply approximating_family_way_below. - apply propproperty. - apply propproperty. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow