proposition: Proposition continuous_dcpo_struct_le_weq_approx_le (x y : X) : x ⊑ y ≃ ∀ (i : approximating_family CX x), approximating_family CX x i ⊑ y.
proof: Proof. use weqimplimpl. - intros p i. apply continuous_dcpo_struct_approx_way_below_to_le. intro j. apply continuous_dcpo_struct_le_to_way_below. exact p. - intros H. apply continuous_dcpo_struct_approx_le_to_le. exact H. - apply propproperty. - apply propproperty. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow