Proposition le_dcpo_specialization_equiv (CX : continuous_dcpo_struct X) (x y : X) : x ⊑ y ≃ x ⊑s y. Proof. use weqimplimpl. - exact le_dcpo_specialization. - intros p. use (invmap (continuous_dcpo_struct_le_via_approximation CX x y)). intro z. intro q. exact (p _ (upper_set_is_scott_open CX z) q). - apply propproperty. - apply propproperty. 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.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.