renaming curry_cvg

math-comp · Nov 14, 2024 · f511831 · f511831
1 parent d7f2bf6
commit f511831
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -99,7 +99,7 @@
   + new lemma `continuous_comp_weak`
 - in file `function_spaces.v`,
   + new definition `eval`
-  + new lemmas `continuous_curry_fun`, `continuous_curry_joint_cvg`, 
+  + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`, 
     `eval_continuous`, and `compose_continuous`
 
 ### Changed

diff --git a/theories/function_spaces.v b/theories/function_spaces.v
@@ -1441,7 +1441,7 @@ Lemma continuous_curry_fun (f : U * V -> W) :
   continuous f -> continuous (curry f).
 Proof. by case/continuous_curry. Qed.
 
-Lemma continuous_curry_joint_cvg (f : U * V -> W) (u : U) (v : V) :
+Lemma continuous_curry_cvg (f : U * V -> W) (u : U) (v : V) :
   continuous f -> curry f z.1 z.2 @[z --> (u, v)] --> curry f u v.
 Proof.
 move=> cf D /cf; rewrite !nbhs_simpl /curry /=; apply: filterS => z ? /=.
@@ -1593,7 +1593,7 @@ have <- : h = uncurry F \o prodAr \o swap.
   by rewrite /h/g/uncurry/swap/F funeqE => -[[]].
 rewrite /h.
 apply: (@continuous2_cvg _ _ _ _ _ _ snd (eval \o fst) (curry eval)).
-- by apply: continuous_curry_joint_cvg; exact: eval_continuous.
+- by apply: continuous_curry_cvg; exact: eval_continuous.
 - exact: cvg_snd.
 - by apply: cvg_comp; [exact: cvg_fst | exact: eval_continuous].
 Qed.