Proposition dcpo_basis_le_via_approximation (x y : X) : x ⊑ y ≃ ∀ (z : B), (B z ≪ x ⇒ B z ≪ y)%logic. Proof. use weqimplimpl. - intros p z q. exact (trans_way_below_le q p). - intros H. rewrite <- (approximating_basis_lub B x). use dcpo_lub_is_least. intro i. apply way_below_to_le. apply (H (pr1 i) (pr2 i)). - apply propproperty. - apply propproperty. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.