From e7696038a74e7b8529b3133d290a93fab0882bf0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 24 Feb 2026 11:15:09 +0900 Subject: [PATCH] fix #1843 --- CHANGELOG_UNRELEASED.md | 4 ++++ theories/function_spaces.v | 5 +++-- theories/normedtype_theory/normed_module.v | 2 +- theories/numfun.v | 6 +++--- theories/topology_theory/subspace_topology.v | 4 ++-- theories/topology_theory/topology_structure.v | 10 +++++++--- 6 files changed, 20 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4aa1cac78..4a2a5998c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -195,6 +195,10 @@ - in `lebesgue_integral_nonneg.v`: + `integral_setD1_EFin` -> `integral_setD1` +- in `topology_structure.v`: + + `closed_comp` -> `preimage_closed` + + `clopen_comp` -> `preimage_clopen` + ### Generalized - in `lebesgue_integral_nonneg.v`: diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 4a6a2937c..9505da948 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1,6 +1,7 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. +From mathcomp Require Import generic_quotient. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. @@ -291,7 +292,7 @@ Proof. move=> dctTI x y /eqP xneqy. have [i/eqP/dctTI [U [clU Ux nUy]]] : exists i, x i <> y i. by apply/existsNP=> W; exact/xneqy/functional_extensionality_dep. -exists (proj i @^-1` U); split => //; apply: clopen_comp => //. +exists (proj i @^-1` U); split => //; apply: preimage_clopen => //. exact/proj_continuous. Qed. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index a564b3525..96cda52d8 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2018,7 +2018,7 @@ Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R) (x : V) (e : R) : closed (closed_ball_ normr x e). Proof. rewrite /closed_ball_ -/((normr \o (fun y => x - y)) @^-1` [set x | x <= e]). -apply: (closed_comp _ (@closed_le _ _)) => y _. +apply: (preimage_closed _ (@closed_le _ _)) => y _. apply: (continuous_comp _ (@norm_continuous _ _ _)). exact: (continuousB (@cst_continuous _ _ _ _)). Qed. diff --git a/theories/numfun.v b/theories/numfun.v index 682438fb7..bc7226be3 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. #[warning="-warn-library-file-internal-analysis"] @@ -1117,8 +1117,8 @@ Proof. move: M => _/posnumP[M] ctsf fA1. have [] := @urysohn_ext_itv (A `&` f @^-1` `]-oo, -(1/3) * M%:num]) (A `&` f @^-1` `[1/3 * M%:num,+oo[) (-(1/3) * M%:num) (1/3 * M%:num). -- by rewrite closed_setSI//; exact: closed_comp. -- by rewrite closed_setSI//; apply: closed_comp => //; exact: interval_closed. +- by rewrite closed_setSI//; exact: preimage_closed. +- by rewrite closed_setSI//; apply: preimage_closed => //; exact: interval_closed. - rewrite setIACA -preimage_setI eqEsubset; split => z // [_ []]. rewrite !set_itvE/= => /[swap] /le_trans /[apply]. by rewrite leNgt mulNr gtrN// mulr_gt0// divr_gt0. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 03f028ea7..d84fb0375 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure uniform_structure compact. @@ -627,7 +627,7 @@ have [fAfE cEIE] : have ? : f @` closure (AfE b) `<=` closure (E b). have /(@image_subset _ _ f) : closure (AfE b) `<=` f @^-1` closure (E b). have /closure_id -> : closed (f @^-1` closure (E b) : set (subspace A)). - by apply: closed_comp => //; exact: closed_closure. + by apply: preimage_closed => //; exact: closed_closure. apply: closure_subset. have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b). by apply: subset_trans A0cA0; apply: subIset; right. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 7eb8bbeae..faab410d9 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -784,7 +784,7 @@ End Closed. #[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_limit_point_isolated` instead")] Notation closure_limit_point := __deprecated__closure_limit_point (only parsing). -Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) : +Lemma preimage_closed {T U : topologicalType} (f : T -> U) (D : set U) : {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D). Proof. rewrite !closedE=> f_continuous D_cl x /= xDf. @@ -793,6 +793,8 @@ have NDfx : ~ D (f x). by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; exact. by apply: f_continuous fxD; rewrite inE. Qed. +#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_closed`")] +Notation closed_comp := preimage_closed (only parsing). Lemma closed_cvg {T} {V : topologicalType} {F} {FF : ProperFilter F} (u_ : T -> V) (A : V -> Prop) : @@ -1006,11 +1008,13 @@ Proof. by split; [exact: open0 | exact: closed0]. Qed. Lemma clopenT {T} : clopen [set: T]. Proof. by split; [exact: openT | exact: closedT]. Qed. -Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) : +Lemma preimage_clopen {T U : topologicalType} (f : T -> U) (A : set U) : clopen A -> continuous f -> clopen (f @^-1` A). -Proof. by case=> ? ?; split; [ exact: open_comp | exact: closed_comp]. Qed. +Proof. by case=> ? ?; split; [ exact: open_comp | exact: preimage_closed]. Qed. End ClopenSets. +#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed to `preimage_clopen`")] +Notation clopen_comp := preimage_clopen (only parsing). HB.mixin Record isContinuous {X Y : nbhsType} (f : X -> Y):= { cts_fun : continuous f