From c0fc1311c4a71527141a0a657ce13ff7f8155592 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 24 Mar 2025 12:47:21 +0100 Subject: [PATCH] adapt to rocq#19987 --- classical/functions.v | 4 ++-- theories/function_spaces.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/classical/functions.v b/classical/functions.v index e40e2819cb..9c89f574c8 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -1734,7 +1734,7 @@ Lemma reindex_bigcup {aT rT I} (f : aT -> I) (P : set aT) (Q : set I) (F : I -> set rT) : set_fun P Q f -> set_surj P Q f -> \bigcup_(x in Q) F x = \bigcup_(x in P) F (f x). Proof. -by move=> /image_subP fPQ /(surj_image_eq fPQ)<-; rewrite bigcup_image. +by move=> /image_subP fPQ /(surj_image_eq fPQ) QE; rewrite -[Q]QE bigcup_image. Qed. Arguments reindex_bigcup {aT rT I} f P Q. @@ -1742,7 +1742,7 @@ Lemma reindex_bigcap {aT rT I} (f : aT -> I) (P : set aT) (Q : set I) (F : I -> set rT) : set_fun P Q f -> set_surj P Q f -> \bigcap_(x in Q) F x = \bigcap_(x in P) F (f x). Proof. -by move=> /image_subP fPQ /(surj_image_eq fPQ)<-; rewrite bigcap_image. +by move=> /image_subP fPQ /(surj_image_eq fPQ) QE; rewrite -[Q]QE bigcap_image. Qed. Arguments reindex_bigcap {aT rT I} f P Q. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 0f257a5685..7e81d8b1e2 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1426,7 +1426,7 @@ Lemma continuous_curry (f : U * V -> W) : continuous (curry f) /\ forall u, continuous (curry f u). Proof. move=> ctsf; split; first last. - move=> u z; apply: continuous_comp; last exact: ctsf. + move=> u z; apply: (continuous_comp _ (ctsf (u, z))). by apply: cvg_pair => //=; exact: cvg_cst. move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. near=> z => w /= [+ + <-]; near: z.