Proposition continuous_dcpo_struct_le_weq_approx_way_below (x y : X) : x ⊑ y ≃ ∀ (i : approximating_family CX x), approximating_family CX x i ≪ y. Proof. use weqimplimpl. - exact continuous_dcpo_struct_le_to_way_below. - intros H. apply continuous_dcpo_struct_approx_le_to_le. intro i. apply continuous_dcpo_struct_approx_way_below_to_le. exact H. - apply propproperty. - apply propproperty. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.