Proposition continuous_dcpo_struct_approx_le_to_le {x y : X} (p : ∏ (i : approximating_family CX x), approximating_family CX x i ⊑ y) : x ⊑ y. Proof. rewrite <- (approximating_family_lub CX x). use dcpo_lub_is_least. exact 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.