Proposition is_scott_open_bin_union {D : dcpo} (P₁ P₂ : scott_open_set D) : is_scott_open (P₁ ∪ P₂). Proof. split. - intros x y. use factor_through_squash_hProp. intros p q. induction p as [ p | p ]. + use hdisj_in1. exact (is_scott_open_upper_set P₁ p q). + use hdisj_in2. exact (is_scott_open_upper_set P₂ p q). - intros A. use factor_through_squash_hProp. intros p. induction p as [ p | p ]. + refine (factor_through_squash_hProp _ _ (is_scott_open_lub_inaccessible P₁ A p)). intros i. induction i as [ i Hi ]. refine (hinhpr (i ,, _)). use hdisj_in1. exact Hi. + refine (factor_through_squash_hProp _ _ (is_scott_open_lub_inaccessible P₂ A p)). intros i. induction i as [ i Hi ]. refine (hinhpr (i ,, _)). use hdisj_in2. exact Hi. 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.