Proposition principal_ideal_way_below {I : rounded_ideal_completion} (b : B) (Hb : b ∈ I) : principal_ideal b ≪ I. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.CompactBasis. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions.