proposition: Proposition complement_of_scott_open (P : X → hProp) (HP : is_scott_open P) : is_scott_closed (λ x, ¬(P x))%logic.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous