Proposition continuous_dcpo_struct_approx_way_below_to_le {x y : X} (p : ∏ (i : approximating_family CX x), approximating_family CX x i ≪ y) (i : approximating_family CX x) : approximating_family CX x i ⊑ y. Proof. use way_below_to_le. apply p. 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.