proposition: Proposition lub_fixpoint (D : directed_set X) (HD : ∏ (d : D), f(D d) = D d) : f (⨆ D) = ⨆ D.
proof: Proof. rewrite scott_continuous_map_on_lub. use antisymm_dcpo. - use dcpo_lub_is_least. intro i ; cbn in i ; cbn. use less_than_dcpo_lub. + exact i. + exact (eq_to_le_dcpo (HD i)). - use dcpo_lub_is_least. intro i ; cbn in i ; cbn. use less_than_dcpo_lub. + exact i. + exact (eq_to_le_dcpo (!(HD i))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Core.ScottContinuous