Definition image_same_lower_bounds {I} (f : I -> P) {x : P} : islowerbound f x <-> islowerbound_subtype (image f) x. Proof. apply (image_carrier_univ' f (fun y => _ ≤ y)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.