proposition: Proposition principal_ideal_way_below {I : rounded_ideal_completion} (b : B) (Hb : b ∈ I) : principal_ideal b ≪ I.
proof: Proof. intros D HD. assert (H := HD _ Hb). revert H. use factor_through_squash_hProp. intro d ; cbn in d. induction d as [ d Hd ]. refine (hinhpr (d ,, _)). cbn ; intros x Hx. exact (is_ideal_lower_set (pr2 (D d)) Hd Hx). 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 UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions