Proposition continuous_dcpo_struct_le_to_way_below {x y : X} (p : x ⊑ y) (i : approximating_family CX x) : approximating_family CX x i ≪ y. Proof. use (trans_way_below_le _ p). apply approximating_family_way_below. 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.