Definition scott_open_set_exp {D : dcpo} (P₁ P₂ : scott_open_set D) : scott_open_set D. Proof. simple refine (scott_open_set_union _). - exact (∑ (Q : scott_open_set D), ∏ (x : D), P₁ x × Q x → P₂ x). - exact pr1. Defined.
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.