From 05aff012dc24df9eef49d6167268a693f3031c5a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 Dec 2023 20:46:38 +0900 Subject: [PATCH 1/2] fixes #1123 Co-authored-by: Takafumi Saikawa Co-authored-by: Zachary Stone --- theories/ereal.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/theories/ereal.v b/theories/ereal.v index 32b7117c7..5be5db40c 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -533,15 +533,21 @@ 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. +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/negP => /eqP/ereal_sup_ninfty/(_ x%:E). +have : (EFin @` A) x%:E by exists x. +by move=> /[swap] /[apply]. 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. From a2ec35bf8e6013a8315bff2aa62046c1c00d68ff Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 26 Dec 2023 14:36:18 +0900 Subject: [PATCH 2/2] fix --- theories/ereal.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/theories/ereal.v b/theories/ereal.v index 5be5db40c..37d007b91 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -536,15 +536,13 @@ Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed 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. +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/negP => /eqP/ereal_sup_ninfty/(_ x%:E). -have : (EFin @` A) x%:E by exists x. -by move=> /[swap] /[apply]. +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) : @@ -565,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].