Proposition is_scott_open_intersection {D : dcpo} (P₁ P₂ : scott_open_set D) : is_scott_open (P₁ ∩ P₂). Proof. split. - intros x y p q. induction p as [ p₁ p₂ ]. split. + exact (is_scott_open_upper_set P₁ p₁ q). + exact (is_scott_open_upper_set P₂ p₂ q). - intros A HA. induction HA as [ HA₁ HA₂ ]. refine (factor_through_squash_hProp _ _ (is_scott_open_lub_inaccessible P₁ A HA₁)). intros i. induction i as [ i Hi ]. refine (factor_through_squash_hProp _ _ (is_scott_open_lub_inaccessible P₂ A HA₂)). intros j. induction j as [ j Hj ]. refine (factor_through_squash_hProp _ _ (directed_set_top A i j)). intros k. induction k as [ k Hk ]. induction Hk as [ Hk₁ Hk₂ ]. refine (hinhpr (k ,, _ ,, _)). + refine (is_scott_open_upper_set P₁ _ Hk₁). exact Hi. + refine (is_scott_open_upper_set P₂ _ Hk₂). exact Hj. 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.