fixes math-comp#1123 (unusable lemma) (math-comp#1124)

* fixes math-comp#1123 Co-authored-by: Takafumi Saikawa <[email protected]> Co-authored-by: Zachary Stone <[email protected]>
affeldt-aist · Dec 27, 2023 · 7dd785b · 7dd785b
1 parent a1fb208
commit 7dd785b
Showing 1 changed file with 11 additions and 7 deletions.
diff --git a/theories/ereal.v b/theories/ereal.v
@@ -533,15 +533,19 @@ Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed
 Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
 Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
 
-Lemma hasNub_ereal_sup (A : set (\bar R)) : ~ has_ubound A ->
-  A !=set0 -> ereal_sup A = +oo%E.
+Lemma hasNub_ereal_sup (A : set R) : ~ has_ubound A ->
+  A !=set0 -> ereal_sup (EFin @` A) = +oo%E.
 Proof.
-move=> hasNubA A0.
-apply/eqP; rewrite eq_le leey /= leNgt; apply: contra_notN hasNubA => Aoo.
-by exists (ereal_sup A); exact: ereal_sup_ub.
+move=> + A0; apply: contra_notP => /eqP; rewrite -ltey => Aoo.
+exists (fine (ereal_sup (EFin @` A))) => x Ax.
+rewrite -lee_fin -(@fineK _ x%:E)// lee_fin fine_le//; last first.
+  by apply: ereal_sup_ub => /=; exists x.
+rewrite fin_numE// -ltey Aoo andbT.
+apply/eqP => /ereal_sup_ninfty/(_ x%:E).
+by have /[swap] /[apply]: (EFin @` A) x%:E by exists x.
 Qed.
 
-Lemma ereal_sup_EFin  (A : set R) :
+Lemma ereal_sup_EFin (A : set R) :
   has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = (sup A)%:E.
 Proof.
 move=> has_ubA A0; apply/eqP; rewrite eq_le; apply/andP; split.
@@ -559,7 +563,7 @@ by rewrite -lee_fin fineK//; apply: ereal_sup_ub; exists r.
 Qed.
 
 Lemma ereal_inf_EFin (A : set R) : has_lbound A -> A !=set0 ->
-   ereal_inf (EFin @` A) = (inf A)%:E.
+  ereal_inf (EFin @` A) = (inf A)%:E.
 Proof.
 move=> has_lbA A0; rewrite /ereal_inf /inf EFinN; congr (- _)%E.
 rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN].