proposition: Proposition le_dcpo_specialization_equiv (CX : continuous_dcpo_struct X) (x y : X) : x ⊑ y ≃ x ⊑s y.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Basis.Continuous