proposition: Proposition dcpo_basis_le_via_approximation (x y : X) : x ⊑ y ≃ ∀ (z : B), (B z ≪ x ⇒ B z ≪ y)%logic.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous