Proposition complement_of_scott_open (P : X → hProp) (HP : is_scott_open P) : is_scott_closed (λ x, ¬(P x))%logic. Proof. split. - cbn ; intros x y p q H. apply p. use (pr1 HP x). + exact H. + exact q. - cbn ; intros D HD p. assert (H := is_scott_open_lub_inaccessible HP D p). revert H. use factor_through_squash. { apply isapropempty. } intro i. induction i as [ i Hi ]. apply (HD i). 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.