Proposition continuous_dcpo_struct_le_via_approximation (x y : X) : x ⊑ y ≃ ∀ (z : X), (z ≪ x ⇒ z ≪ y)%logic. Proof. use weqimplimpl. - intros p z q. exact (trans_way_below_le q p). - intros H. rewrite <- (approximating_family_lub CX x). use dcpo_lub_is_least. pose (D := approximating_family CX x). fold D. intro i. apply way_below_to_le. apply (H (D i)). apply approximating_family_way_below. - 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.