proposition: Proposition is_scott_continuous_incl (x : X) : is_scott_continuous (Y x) coproduct_set_dcpo (λ y, x ,, y).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous