From 6be0f8ad7ba6430d76aaee8d3daa2213e65f9fdb 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/2] 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 a0f9ee484..11f0ff929 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -705,3 +705,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 e0e1e4ee8c55d31a71a08df147906cdd3c005cfb 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/2] changelog

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f4a1cc4df..3ddd0c5fd 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -70,6 +70,9 @@
 - in `derive.v`:
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
+- in `subspace_topology.v`:
+  + lemma `within_continuous_patch`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.