Proposition is_scott_continuous_map_from_discrete_dcpo {A : hSet} {X : dcpo} (f : A → X) : is_scott_continuous (pr2 (discrete_dcpo A)) (pr2 X) f. Proof. use make_is_scott_continuous. - apply (pr2 (monotone_function_discrete_dcpo X f)). - intros D. assert (H := directed_set_el D). revert H. use factor_through_squash. { apply setproperty. } cbn ; intros i. rewrite (discrete_dcpo_lub D i). use antisymm_dcpo. + use less_than_dcpo_lub. * exact i. * cbn. apply refl_dcpo. + use dcpo_lub_is_least. intro j ; cbn. cbn in *. assert (H := directed_set_top D i j). revert H. use factor_through_squash. { apply propproperty. } cbn ; intros H. induction H as [ k [ p q ]]. rewrite p, q. apply refl_dcpo. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.