Proposition upper_set_is_scott_open (CX : continuous_dcpo_struct X) (x : X) : is_scott_open (way_below_upper_set x). 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.