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. 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.
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.