Proposition scott_continuous_map_on_lub {X Y : dcpo} (f : scott_continuous_map X Y) (D : directed_set X) : f (⨆ D) = ⨆_{D} f. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness.