Lemma is_sharp_to_le {X : dcpo} (CX : continuous_dcpo_struct X) {x y : X} (Hy : is_sharp y) (p : ¬(x ⊄ y)) : x ⊑ y. Proof. use (invmap (continuous_dcpo_struct_le_via_approximation CX x y)). intros z q. assert (H := unary_interpolation CX q). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ u [ r₁ r₂ ]]. assert (H := Hy _ _ r₁). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ s | s ]. - exact s. - cbn in s. refine (fromempty (p _)). refine (hinhpr (_ ,, upper_set_is_scott_open CX u ,, r₂ ,, _)). intro w. apply s. apply way_below_to_le. exact w. 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.Core.IntrinsicApartness. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.