proposition: Proposition is_continuous_dcpo_directed_set_lub {X : dcpo} (CX : is_continuous_dcpo X) (x : X) : ⨆ (is_continuous_dcpo_directed_set CX x) = x.
proof: Proof. revert CX. use factor_dep_through_squash. { intro. apply setproperty. } intros CX. pose (D := approximating_family CX x). cbn. use antisymm_dcpo. - use dcpo_lub_is_least. intros i. apply way_below_to_le. exact (pr2 i). - refine (trans_dcpo _ _). { apply eq_to_le_dcpo. exact (!(approximating_family_lub CX x)). } use dcpo_lub_is_least. intros i. use less_than_dcpo_lub ; cbn -[way_below]. + refine (D i ,, _). apply approximating_family_way_below. + apply refl_dcpo. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow