Proposition continuous_dcpo_struct_way_below (x y : X) : x ≪ y ≃ ∃ (i : approximating_family CX y), x ⊑ approximating_family CX y i. 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.
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.