From 7dd785b74da949bdde062f9e25f8107d9f5e3ae4 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 26 Dec 2023 18:25:23 +0900 Subject: [PATCH] fixes #1123 (unusable lemma) (#1124) * fixes #1123 Co-authored-by: Takafumi Saikawa Co-authored-by: Zachary Stone --- theories/ereal.v | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/theories/ereal.v b/theories/ereal.v index 7312a3773..ec7674324 100644 --- 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].