Definition false_scott_open_set (A : dcpo) : scott_open_set A. Proof. simple refine (_ ,, _). - exact (λ _, hfalse). - split. + abstract (intros x y p q; exact (fromempty p)). + abstract (intros D p; exact (fromempty p)). 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.