proposition: Proposition basis_unary_interpolation {x y : X} (p : x ≪ y) : ∃ (i : B), x ≪ B i ∧ B i ≪ y.
proof: Proof. assert (H := unary_interpolation CX p). revert H. use factor_through_squash. { apply propproperty. } intro z. induction z as [ z [ q₁ q₂ ] ]. assert (r : y ⊑ ⨆ directed_set_from_basis B y). { rewrite approximating_basis_lub. apply refl_dcpo. } assert (H := q₂ (directed_set_from_basis B y) r). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ [ i s₁ ] s₂ ]. refine (hinhpr (i ,, _ ,, _)). - exact (trans_way_below_le q₁ s₂). - exact s₁. 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