proposition: Proposition upper_set_is_scott_open (CX : continuous_dcpo_struct X) (x : X) : is_scott_open (λ y, x ≪ y).
proof: Proof. split. - intros y₁ y₂ p q. exact (trans_way_below_le p q). - intros D p. assert (H := unary_interpolation CX p). revert H. use factor_through_squash. { apply propproperty. } intro z. induction z as [ z [ q₁ q₂ ]]. assert (H := q₂ D (refl_dcpo _)). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ i r ]. refine (hinhpr (i ,, _)). exact (trans_way_below_le q₁ r). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous