From 295f076ec71b72f9b5b56285d93f868aac2ca1e8 Mon Sep 17 00:00:00 2001
From: Holger Thies <info@holgerthies.com>
Date: Thu, 5 Mar 2026 19:45:10 +0900
Subject: [PATCH 1/3] added within_continuous_patch

---
 theories/topology_theory/subspace_topology.v | 24 ++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index 36019a2d01..df72b1fa72 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -711,3 +711,27 @@ HB.instance Definition _ :=
   @isContinuous.Build (subspace A) Z (g \o f) continuous_comp_subproof.
 
 End continuous_fun_comp.
+
+Section continuous_patch.
+Context {U : topologicalType} {V : topologicalType}.
+Variables (A : set U) (B : set U) (f : U -> V) (g : U -> V).
+Hypothesis cont1 : {within A, continuous f}.
+Hypothesis cont2 : {within B, continuous g}.
+Hypothesis closedA : closed A.
+Hypothesis closedB : closed B.
+Hypothesis eq_AB : forall x, x \in A `&` B -> f x = g x.  
+
+Lemma within_continuous_patch : {within A `|` B, continuous (patch g A f)}.
+Proof.
+apply: withinU_continuous => //.
+  have : {in A, f =1 patch g A f } by rewrite /patch => r ->.
+  by move/subspace_eq_continuous; apply.
+have : {in B, g =1 patch g A f }.
+  move=> r rab.
+  rewrite /patch; case: ifPn => [xab | //].
+  apply/esym/eq_AB.
+  by rewrite inE; split; apply set_mem.
+by move/subspace_eq_continuous; apply.
+Qed.
+
+End continuous_patch.

From 7df8027f1b84c56833a8e4afa02ac61f20ac3941 Mon Sep 17 00:00:00 2001
From: Holger Thies <info@holgerthies.com>
Date: Thu, 5 Mar 2026 19:48:28 +0900
Subject: [PATCH 2/3] changelog

---
 CHANGELOG_UNRELEASED.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ff11a74fa8..f2a68c63b0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -81,6 +81,9 @@
 - in `measurable_structure.v`:
   + structure `PMeasurable`, notation `pmeasurableType`
 
+- in `subspace_topology.v`:
+  + lemma `within_continuous_patch`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

From 55048bd4c40d0aa6fd40b2ab3e450d603a135b07 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 1 May 2026 09:01:26 +0900
Subject: [PATCH 3/3] linting

---
 CHANGELOG_UNRELEASED.md                      |  2 +-
 theories/topology_theory/subspace_topology.v | 26 +++++++++-----------
 2 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f2a68c63b0..ff77886603 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -82,7 +82,7 @@
   + structure `PMeasurable`, notation `pmeasurableType`
 
 - in `subspace_topology.v`:
-  + lemma `within_continuous_patch`
+  + lemma `withinU_continuous_patch`
 
 ### Changed
 
diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index df72b1fa72..3fd9350720 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -713,25 +713,23 @@ HB.instance Definition _ :=
 End continuous_fun_comp.
 
 Section continuous_patch.
-Context {U : topologicalType} {V : topologicalType}.
-Variables (A : set U) (B : set U) (f : U -> V) (g : U -> V).
-Hypothesis cont1 : {within A, continuous f}.
-Hypothesis cont2 : {within B, continuous g}.
+Context {U V : topologicalType}.
+Variables (A B : set U) (f g : U -> V).
+Hypothesis contf : {within A, continuous f}.
+Hypothesis contg : {within B, continuous g}.
 Hypothesis closedA : closed A.
 Hypothesis closedB : closed B.
-Hypothesis eq_AB : forall x, x \in A `&` B -> f x = g x.  
+Hypothesis AB_fg : forall x, x \in A `&` B -> f x = g x.
 
-Lemma within_continuous_patch : {within A `|` B, continuous (patch g A f)}.
+Lemma withinU_continuous_patch : {within A `|` B, continuous (patch g A f)}.
 Proof.
+pose gAf := patch g A f.
 apply: withinU_continuous => //.
-  have : {in A, f =1 patch g A f } by rewrite /patch => r ->.
-  by move/subspace_eq_continuous; apply.
-have : {in B, g =1 patch g A f }.
-  move=> r rab.
-  rewrite /patch; case: ifPn => [xab | //].
-  apply/esym/eq_AB.
-  by rewrite inE; split; apply set_mem.
-by move/subspace_eq_continuous; apply.
+- suff : {in A, f =1 gAf} by move/subspace_eq_continuous; exact.
+  by rewrite /gAf /patch => r ->.
+- suff : {in B, g =1 gAf} by move/subspace_eq_continuous; exact.
+  move=> r rB; rewrite /gAf /patch; case: ifPn => // rA.
+  by apply/esym/AB_fg; rewrite in_setI rA.
 Qed.
 
 End continuous_patch.