proposition: Proposition scott_continuous_map_on_lub {X Y : dcpo} (f : scott_continuous_map X Y) (D : directed_set X) : f (⨆ D) = ⨆_{D} f.
proof: Proof. refine (is_scott_continuous_on_lub (pr2 f) _ (pr22 D) @ _). use (eq_lub Y (f {{ D }})). - use make_dcpo_is_least_upperbound. + cbn ; intro i. exact (lub_is_upperbound (dcpo_struct_lub Y _ (is_directed_comp (pr1 f) (pr12 f) (pr22 D))) i). + intros x Hx. exact (lub_is_least (dcpo_struct_lub Y _ (is_directed_comp (pr1 f) (pr12 f) (pr22 D))) x Hx). - apply is_least_upperbound_dcpo_comp_lub. 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.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness