Proposition is_scott_continuous_incl (x : X) : is_scott_continuous (Y x) coproduct_set_dcpo (λ y, x ,, y). Proof. use make_is_scott_continuous. - exact (λ y₁ y₂ p, is_monotone_set_in Y Y x y₁ y₂ p). - intro D ; cbn. use (eq_lub coproduct_set_dcpo (directed_set_comp (set_in_monotone_function Y Y x) D)). + exact (pr2 (coproduct_dcpo_incl_lub x D)). + exact (is_least_upperbound_dcpo_comp_lub _ D). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.