proposition: Proposition unary_interpolation_cofinal_lem {i₁ i₂ : D} (q : D i₁ ⊑ D i₂) (j₁ : D_a i₁) : D_a i₁ j₁ ≪ ⨆ (D_a i₂).
proof: Proof. refine (trans_way_below_le _ _). - apply approximating_family_way_below. - refine (trans_dcpo q _). unfold D_a. rewrite approximating_family_lub. apply refl_dcpo. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow