From 0a4bd65fa24a07723d095f24b97682c66af78f55 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 21 Jun 2024 00:56:25 +0900
Subject: [PATCH] fixes #1231

---
 CHANGELOG_UNRELEASED.md |  8 ++++++++
 theories/topology.v     | 13 +++++++++----
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index fb0dceb258..3bd10f2be8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,8 +4,16 @@
 
 ### Added
 
+- in `topology.v`:
+  + lemma `ball_subspace_ball`
+
 ### Changed
 
+- in `topology.v`:
+  + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
+    `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
+	into local `Let`'s
+
 ### Renamed
 
 - in `constructive_ereal.v`:
diff --git a/theories/topology.v b/theories/topology.v
index c92ca0ad37..82834994df 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6403,17 +6403,18 @@ End SubspaceUniform.
 
 Section SubspacePseudoMetric.
 Context {R : numDomainType} {X : pseudoMetricType R} (A : set X).
+Implicit Type e : R.
 
 Definition subspace_ball (x : subspace A) (r : R) :=
   if x \in A then A `&` ball (x : X) r else [set x].
 
-Lemma subspace_pm_ball_center x (e : R) : 0 < e -> subspace_ball x e x.
+Let subspace_pm_ball_center x e : 0 < e -> subspace_ball x e x.
 Proof.
 rewrite /subspace_ball; case: ifP => //= /asboolP ? ?.
 by split=> //; exact: ballxx.
 Qed.
 
-Lemma subspace_pm_ball_sym x y (e : R) :
+Let subspace_pm_ball_sym x y e :
   subspace_ball x e y -> subspace_ball y e x.
 Proof.
 rewrite /subspace_ball; case: ifP => //= /asboolP ?.
@@ -6421,7 +6422,7 @@ rewrite /subspace_ball; case: ifP => //= /asboolP ?.
 by move=> ->; case: ifP => /asboolP.
 Qed.
 
-Lemma subspace_pm_ball_triangle x y z e1 e2 :
+Let subspace_pm_ball_triangle x y z e1 e2 :
   subspace_ball x e1 y -> subspace_ball y e2 z -> subspace_ball x (e1 + e2) z.
 Proof.
 rewrite /subspace_ball; (repeat case: ifP => /asboolP).
@@ -6431,7 +6432,7 @@ rewrite /subspace_ball; (repeat case: ifP => /asboolP).
 - by move=> _ _ -> ->.
 Qed.
 
-Lemma subspace_pm_entourageE :
+Let subspace_pm_entourageE :
   @entourage (subspace A) = entourage_ subspace_ball.
 Proof.
 rewrite eqEsubset; split; rewrite /subspace_ball.
@@ -6452,6 +6453,10 @@ HB.instance Definition _ :=
     subspace_pm_ball_center subspace_pm_ball_sym subspace_pm_ball_triangle
     subspace_pm_entourageE.
 
+Lemma ball_subspace_ball (x : subspace A) r (y : subspace A) :
+  ball x r y = subspace_ball x r y.
+Proof. by []. Qed.
+
 End SubspacePseudoMetric.
 
 Section SubspaceWeak.