Lemma leastfixedpoint_isleast {D : dcpowithbottom} (f : D --> D) : ∏ (d : D), ((pr1 f) d ≤ d) -> (pr1 μ f ≤ d). Proof. intros d ineq. eapply islub_isleast. - apply pointwiselub_islubpointwise. - intro n; induction n as [ | m IH]. + apply dcpowithbottom_isMinimal. + unfold pointwisefamily. simpl. eapply istrans_posetRelation. * apply dcpomorphism_preservesorder. exact IH. * exact ineq. Qed.
Require Import UniMath.Foundations.All.