From 8db04a2f13540ea71ad248551ceddcfb0281e4e9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 19 Mar 2026 19:23:13 +0900
Subject: [PATCH] closure of an open interval

---
 CHANGELOG_UNRELEASED.md                                |  9 +++++++++
 theories/normedtype_theory/normed_module.v             |  9 +++++++++
 .../normedtype_theory/pseudometric_normed_Zmodule.v    | 10 ++++++++++
 3 files changed, 28 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..ca17283f10 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,15 @@
 
 ### Added
 
+- in `realfun.v`:
+  + lemma `derivable_sqrt`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `itv_center_shift`
+
+- in `normed_module.v`:
+  + lemmas `closure_itvoo`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index bcc6e52fd4..cf194d12b8 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -2082,6 +2082,15 @@ Qed.
 
 End Closed_Ball_normedModType.
 
+(* NB: see also itv_closure *)
+Lemma closure_itvoo (R : realFieldType) (a b : R) : a < b ->
+  closure `]a, b[%classic = `[a, b]%classic.
+Proof.
+move=> ab.
+rewrite itv_center_shift// -ball_itv closure_ballE itv_center_shift//.
+by rewrite closed_ball_itv// divr_gt0// subr_gt0.
+Qed.
+
 Lemma open_subball {R : numFieldType} {M : normedModType R} (A : set M)
   (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
 Proof.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 687d6f3f6b..c09977463f 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -97,6 +97,16 @@ End Shift.
 Arguments shift {R} x / y.
 Notation center c := (shift (- c)).
 
+Lemma itv_center_shift {R : numFieldType} x y (a b : R) : (a < b) ->
+  let c := (a + b) / 2 in let r := (b - a) / 2 in
+  Interval (BSide x a) (BSide y b) =
+  Interval (BSide x (center r c (*c - r*) )) (BSide y (shift r c (*c + r*))).
+Proof.
+move=> ab c r; rewrite /shift /c /r -mulrBl addrKA opprK -mulrDl.
+rewrite [in X in _ = Interval _ X]addrC subrKA -!mulr2n.
+by rewrite -(mulr_natr a) -(mulr_natr b) !mulfK.
+Qed.
+
 Section at_left_right_topologicalType.
 Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).