From 12b620ee8baa69016877b36d253147f7486ae3a6 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 14 Jan 2021 13:27:11 +0900
Subject: [PATCH] lemmas to prove inf/sup properties of intervals

---
 CHANGELOG_UNRELEASED.md   |  3 +++
 theories/classical_sets.v |  6 ++++++
 theories/reals.v          | 19 +++++++++++++++++++
 3 files changed, 28 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1a823194bc..313ca10ebe 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -14,6 +14,9 @@
   `closed_ball_closed`, `closed_ball_subset`, `nbhs_closedballP`, `subset_closed_ball`
 
 - in `normedtype.v`, lemmas `nbhs0_lt`, `nbhs'0_lt`, `interior_closed_ballE`, open_nbhs_closed_ball`
+- in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound`
+
+- in `reals.v`, lemmas `sup_setU`, `inf_setU`
 
 ### Changed
 
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index 6ae881e899..727f0cd1b4 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -1136,6 +1136,12 @@ Definition has_sup E := E !=set0 /\ has_ubound E.
 Definition has_lbound  E := lbound E !=set0.
 Definition has_inf E := E !=set0 /\ has_lbound E.
 
+Lemma subset_has_lbound A B : A `<=` B -> has_lbound B -> has_lbound A.
+Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
+
+Lemma subset_has_ubound A B : A `<=` B -> has_ubound B -> has_ubound A.
+Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
+
 Lemma has_ub_set1 x : has_ubound [set x].
 Proof. by exists x; rewrite ub_set1. Qed.
 
diff --git a/theories/reals.v b/theories/reals.v
index d774176722..cd4f02cb28 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -402,6 +402,17 @@ move=> nzE; split=> [/asboolPn|/has_ubPn h [_]] //.
 by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_ubPn.
 Qed.
 
+Lemma sup_setU (A B : set R) : has_sup B ->
+  (forall a b, A a -> B b -> a <= b) -> sup (A `|` B) = sup B.
+Proof.
+move=> [B0 [l Bl]] AB; apply/eqP; rewrite eq_le; apply/andP; split.
+- apply sup_le_ub => [|x [Ax|]]; first by apply: subset_nonempty B0 => ?; right.
+  by case: B0 => b Bb; rewrite (le_trans (AB _ _ Ax Bb)) // sup_ub //; exists l.
+- by move=> Bx; rewrite sup_ub //; exists l.
+- apply sup_le_ub => // b Bb; apply sup_ub; last by right.
+  by exists l => x [Ax|Bx]; [rewrite (le_trans (AB _ _ Ax Bb)) // Bl|exact: Bl].
+Qed.
+
 End RealLemmas.
 
 (* -------------------------------------------------------------------- *)
@@ -454,6 +465,14 @@ move=> nzE; split=> [/asboolPn|/has_lbPn h [_] //].
 by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_lbPn.
 Qed.
 
+Lemma inf_setU (A B : set R) : has_inf A ->
+  (forall a b, A a -> B b -> a <= b) -> inf (A `|` B) = inf A.
+Proof.
+move=> hiA AB; congr (- _).
+rewrite image_setU setUC sup_setU //; first exact/has_inf_supN.
+by move=> _ _ [] b Bb <-{} [] a Aa <-{}; rewrite ler_oppl opprK; apply AB.
+Qed.
+
 End InfTheory.
 
 (* -------------------------------------------------------------------- *)