From 3dfb6c8ac6caec71ae7b4ff654df0a9741953d74 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2026 22:33:10 +0900 Subject: [PATCH 1/4] fixes #1998 --- theories/pi_irrational.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index fd64178618..7ca2cba748 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -395,7 +395,7 @@ End analytic_part. End pi_irrational. -Lemma pi_irrationnal {R : realType} : ~ rational (pi : R). +Lemma pi_irrational {R : realType} : ~ rational (pi : R). Proof. move/rationalP => [a [b]]; have [->|b0 piratE] := eqVneq b O. by rewrite invr0 mulr0; apply/eqP; rewrite gt_eqF// pi_gt0. From 246d568b26fbea5f2d0b861d7182815b16af4aab Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2026 22:35:04 +0900 Subject: [PATCH 2/4] partly address issue 1968 --- theories/topology_theory/topology_structure.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index ed7536d335..1006a5edfd 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -29,8 +29,6 @@ From mathcomp Require Export filter. (* second_countable T == T has a countable basis *) (* [locally P] := forall a, A a -> G (within A (nbhs x)) if P *) (* is convertible to G (globally A) *) -(* finI_from D f == set of \bigcap_(i in E) f i where E is a *) -(* finite subset of D *) (* U° == all of the points which are locally in U, *) (* i.e., the largest open set contained in U *) (* This is a notation for `interior U`. *) From 010e5da2d90691044f497aac407220f7f4a418f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2026 22:40:15 +0900 Subject: [PATCH 3/4] partly address issue 1967 --- CHANGELOG_UNRELEASED.md | 4 ++++ classical/classical_sets.v | 6 ++++++ theories/measure_theory/measurable_structure.v | 17 ----------------- theories/topology_theory/subspace_topology.v | 2 +- 4 files changed, 11 insertions(+), 18 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1100d1bebb..134a34eefb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -303,6 +303,10 @@ - in `measurable_structure.v`: + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR` +- file `measurable_structure.v`: + + notations `preimage_class`, `image_class`, `sigma_algebra_preimage_class`, + `sigma_algebra_image_class`, `sigma_algebra_preimage_classE` (deprecated since 1.9.0) + ### Infrastructure ### Misc diff --git a/classical/classical_sets.v b/classical/classical_sets.v index b19cdca9e1..b166a3fd0a 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -108,6 +108,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* rectangle X Y := [set U `*` V | U in X & V in Y] *) (* preimage_set_system D f G == set system of the preimages by f of sets *) (* in G *) +(* image_set_system D f G == set system of the sets with a preimage *) +(* by f in G *) (* cross f g X Y := preimage_set_system setT f X *) (* `|` preimage_set_system setT g Y *) (* X `x` Y := cross fst snd X Y *) @@ -1717,6 +1719,10 @@ Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) : preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B. Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed. +Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) + (G : set (set aT)) : set (set rT) := + [set B : set rT | G (D `&` f @^-1` B)]. + Section cross. Context {T T1 T2 : Type}. Implicit Types (X : set_system T1) (Y : set_system T2). diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index fe676545ac..9b403ca563 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -98,8 +98,6 @@ From mathcomp Require Import ereal topology normedtype sequences. (* This is an HB alias. *) (* f.-preimage.-measurable A == A is measurable for *) (* g_sigma_algebra_preimage f *) -(* image_set_system D f G == set system of the sets with a preimage *) -(* by f in G *) (* subset_sigma_subadditive mu == alternative predicate defining *) (* sigma-subadditivity *) (* ``` *) @@ -1380,10 +1378,6 @@ Notation "f .-preimage" := (preimage_display f) : measure_display_scope. Notation "f .-preimage.-measurable" := (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope. -Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT) - (G : set (set aT)) : set (set rT) := - [set B : set rT | G (D `&` f @^-1` B)]. - Lemma sigma_algebra_image (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : sigma_algebra D G -> sigma_algebra setT (image_set_system D f G). @@ -1423,17 +1417,6 @@ by move=> _ [B mB <-]; exact: sG'sfun. Qed. End measurability. -#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system`")] -Notation preimage_class := preimage_set_system (only parsing). -#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `image_set_system`")] -Notation image_class := image_set_system (only parsing). -#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_preimage`")] -Notation sigma_algebra_preimage_class := sigma_algebra_preimage (only parsing). -#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_image`")] -Notation sigma_algebra_image_class := sigma_algebra_image (only parsing). - -#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")] -Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing). (** This predicate is used also by `measure_function.v` *) Definition subset_sigma_subadditive {T} {R : numFieldType} diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 3fd9350720..efab8ebfe2 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -603,7 +603,7 @@ Lemma connected_continuous_connected (T U : topologicalType) connected A -> {within A, continuous f} -> connected (f @` A). Proof. move=> cA cf; apply: contrapT => /connectedPn[E [E0 fAE sE]]. -set AfE := fun b =>(A `&` f @^-1` E b) : set (subspace A). +set AfE := fun b => (A `&` f @^-1` E b) : set (subspace A). suff sAfE : separated (AfE false) (AfE true). move: cA; apply/connectedPn; exists AfE; split; last (rewrite /AfE; split). - move=> b; case: (E0 b) => /= u Ebu. From 9486fec36abd4791dbba754d95dcb2e861beaa06 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2026 23:41:53 +0900 Subject: [PATCH 4/4] fixes #1957 --- classical/filter.v | 2 +- classical/functions.v | 2 +- classical/mathcomp_extra.v | 2 +- experimental_reals/discrete.v | 2 +- experimental_reals/distr.v | 2 +- experimental_reals/realseq.v | 2 +- experimental_reals/realsum.v | 2 +- experimental_reals/xfinmap.v | 2 +- reals/constructive_ereal.v | 2 +- reals/reals.v | 2 +- reals_stdlib/Rstruct.v | 2 +- theories/borel_hierarchy.v | 2 +- theories/ereal.v | 2 +- theories/ess_sup_inf.v | 2 +- theories/hoelder.v | 4 ++-- theories/homotopy_theory/continuous_path.v | 2 +- theories/homotopy_theory/wedge_sigT.v | 2 +- theories/lebesgue_integral_theory/giry.v | 2 +- theories/measure_theory/counting_measure.v | 2 +- theories/measure_theory/dirac_measure.v | 2 +- theories/measure_theory/measurable_function.v | 2 +- theories/measure_theory/measurable_structure.v | 2 +- theories/measure_theory/measure_extension.v | 2 +- theories/measure_theory/measure_function.v | 2 +- theories/measure_theory/measure_negligible.v | 2 +- theories/measure_theory/probability_measure.v | 2 +- theories/normedtype_theory/normed_module.v | 14 +++++++------- theories/normedtype_theory/tvs.v | 2 +- theories/numfun.v | 8 ++++---- theories/pi_irrational.v | 2 +- theories/topology_theory/bool_topology.v | 2 +- theories/topology_theory/compact.v | 2 +- theories/topology_theory/connected.v | 2 +- theories/topology_theory/discrete_topology.v | 3 ++- theories/topology_theory/function_spaces.v | 6 +++--- theories/topology_theory/initial_topology.v | 18 ++++++++++-------- theories/topology_theory/matrix_topology.v | 2 +- theories/topology_theory/nat_topology.v | 2 +- theories/topology_theory/num_topology.v | 2 +- .../one_point_compactification.v | 2 +- theories/topology_theory/order_topology.v | 2 +- theories/topology_theory/product_topology.v | 2 +- .../topology_theory/pseudometric_structure.v | 2 +- theories/topology_theory/quotient_topology.v | 2 +- theories/topology_theory/separation_axioms.v | 2 +- theories/topology_theory/sigT_topology.v | 2 +- theories/topology_theory/subspace_topology.v | 2 +- theories/topology_theory/subtype_topology.v | 2 +- theories/topology_theory/supremum_topology.v | 2 +- theories/topology_theory/topology_structure.v | 2 +- theories/topology_theory/uniform_structure.v | 2 +- theories/topology_theory/weak_topology.v | 2 +- 52 files changed, 74 insertions(+), 71 deletions(-) diff --git a/classical/filter.v b/classical/filter.v index 172c8ac6d0..4eae1af6cf 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. diff --git a/classical/functions.v b/classical/functions.v index 588489d5c7..994baaac34 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2656,7 +2656,7 @@ Let mulrC : commutative (@GRing.mul (T -> M)). Proof. by move=> f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC. Qed. HB.instance Definition _ := - GRing.PzRing_hasCommutativeMul.Build (T -> M) mulrC. + GRing.SemiRing_hasCommutativeMul.Build (T -> M) mulrC. End fct_comPzRingType. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index d3a14ce6e8..2c2c258b22 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat finmap all_algebra. +From mathcomp Require Import all_ssreflect_compat finmap algebra. (**md**************************************************************************) (* # MathComp extra *) diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 948cbb614f..40fdca134b 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -6,7 +6,7 @@ (* -------------------------------------------------------------------- *) From Corelib Require Setoid. From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp.classical Require Import boolp. From mathcomp Require Import xfinmap reals. diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 26f82b3ef8..1e0d73252c 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp.classical Require Import boolp classical_sets mathcomp_extra. From mathcomp Require Import xfinmap constructive_ereal reals discrete. From mathcomp Require Import realseq realsum. diff --git a/experimental_reals/realseq.v b/experimental_reals/realseq.v index 394ccdf284..879841103f 100644 --- a/experimental_reals/realseq.v +++ b/experimental_reals/realseq.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import bigenough. From mathcomp.classical Require Import boolp classical_sets functions. From mathcomp.classical Require Import mathcomp_extra. diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 267b1b7688..20f9eaf1d6 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -3,7 +3,7 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp.classical Require Import boolp. diff --git a/experimental_reals/xfinmap.v b/experimental_reals/xfinmap.v index 80d1a5a1f6..f0773fa7a8 100644 --- a/experimental_reals/xfinmap.v +++ b/experimental_reals/xfinmap.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Export finmap. Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index cea1c06ff2..a3fb1dc399 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -10,7 +10,7 @@ incorporate it into mathcomp proper where it could then be used for bounds of intervals*) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import mathcomp_extra interval_inference. (**md**************************************************************************) diff --git a/reals/reals.v b/reals/reals.v index c05603f075..3e73e62d96 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -44,7 +44,7 @@ (******************************************************************************) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index e7c6250483..8a104bb8dd 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -106,7 +106,7 @@ HB.instance Definition _ := GRing.Zmodule_isNzRing.Build R RmultA Rmult_1_l Rmult_1_r Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0. #[hnf] -HB.instance Definition _ := GRing.PzRing_hasCommutativeMul.Build R Rmult_comm. +HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build R Rmult_comm. Import Monoid. diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index c7c116d498..9fc7243db5 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals topology normedtype sequences. From mathcomp Require Import measure lebesgue_measure measurable_realfun. diff --git a/theories/ereal.v b/theories/ereal.v index 76dfc1b728..b69e6e3aff 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -5,7 +5,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 88f2e0ebc2..160532919b 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals ereal topology normedtype sequences. From mathcomp Require Import measure lebesgue_measure measurable_realfun. diff --git a/theories/hoelder.v b/theories/hoelder.v index 5efca44b13..09354d0982 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -884,7 +884,7 @@ Proof. by move=> a/= f; rewrite !inE; exact: measurable_funM. Qed. HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) mfun_scaler_closed. -HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. +HB.instance Definition _ := [SubNmodule_isSubLSemiModule of {mfun T >-> R} by <:]. End mfun_extra. @@ -962,7 +962,7 @@ HB.instance Definition _ := GRing.isOppClosed.Build _ Lfun Lfun_oppr_closed. (* NB: not used directly by HB.instance *) -Lemma Lfun_addr_closed : addr_closed Lfun. +Lemma Lfun_addr_closed : Algebra.nmod_closed Lfun. Proof. split. by rewrite inE rpred0/= inE/=; exact: finite_norm_cst0. diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index 7817369969..7dfccbf51b 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat generic_quotient all_algebra. +From mathcomp Require Import all_ssreflect_compat generic_quotient algebra. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index f9eba3aec2..8e6e196cde 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra generic_quotient. +From mathcomp Require Import all_ssreflect_compat algebra generic_quotient. From mathcomp Require Import finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index d782c8080d..e3c6b24c45 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -1,5 +1,5 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra boolp classical_sets. +From mathcomp Require Import all_ssreflect_compat algebra boolp classical_sets. From mathcomp Require Import fsbigop functions reals topology separation_axioms. From mathcomp Require Import ereal sequences numfun measure measurable_realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral. diff --git a/theories/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v index 65b1dbe0ff..8b6a8198ab 100644 --- a/theories/measure_theory/counting_measure.v +++ b/theories/measure_theory/counting_measure.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import interval_inference ereal topology normedtype. From mathcomp Require Import sequences measurable_structure measure_function. diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v index d2e8cea15a..60f7266606 100644 --- a/theories/measure_theory/dirac_measure.v +++ b/theories/measure_theory/dirac_measure.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop reals. From mathcomp Require Import interval_inference ereal topology normedtype. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 48f7b50673..061d3b958c 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 9b403ca563..dd71a6733a 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index 7f1bd77611..d8cd41bdeb 100644 --- a/theories/measure_theory/measure_extension.v +++ b/theories/measure_theory/measure_extension.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals interval_inference ereal topology normedtype. From mathcomp Require Import sequences esum. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index d8a4ac0721..dd0a33feaa 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. diff --git a/theories/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v index 442c4f82ea..1e0ce95855 100644 --- a/theories/measure_theory/measure_negligible.v +++ b/theories/measure_theory/measure_negligible.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 42aae61f2e..4d32eff27c 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import interval_inference ereal topology normedtype. From mathcomp Require Import measurable_structure measure_function dirac_measure. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index cdf8d7fda5..31c99d1a4f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -186,7 +186,7 @@ Module numFieldNormedType. Section realType. Variable (R : realType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -196,7 +196,7 @@ End realType. Section rcfType. Variable (R : rcfType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -206,7 +206,7 @@ End rcfType. Section archiFieldType. Variable (R : archiRealFieldType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -216,7 +216,7 @@ End archiFieldType. Section realFieldType. Variable (R : realFieldType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -228,7 +228,7 @@ End realFieldType. Section numClosedFieldType. Variable (R : numClosedFieldType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -240,7 +240,7 @@ End numClosedFieldType. Section numFieldType. Variable (R : numFieldType). #[export, non_forgetful_inheritance] -HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o. #[export, non_forgetful_inheritance] HB.instance Definition _ := Vector.copy R R^o. #[export, non_forgetful_inheritance] @@ -2727,7 +2727,7 @@ have NC0 : continuous (N : max_space V -> R). by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0]. have: compact [set x : max_space V | `|x| = 1]. apply: (subclosed_compact _ (@sup_closed_ball_compact V)). - - apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. + - apply: (@preimage_closed _ _ _ [set 1 : R]); last exact: closed_eq. by move=> *; exact: norm_continuous. - by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->. move=> /(@continuous_compact _ _ (N : max_space V -> R)) -/(_ _)/wrap[]. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 01882c6196..41126a781d 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -472,7 +472,7 @@ exists [set a | exists2 b, B b & \val @^-1` b = a]. - by move: ra; rewrite -ba !inE. - by move: sa; rewrite -ba !inE. split => /=. - move=> a/= [b Bb <-]; rewrite /open/= /wopen/=; exists b => //. + move=> a/= [b Bb <-]; rewrite /open/= /initial_open/=; exists b => //. exact: openB. move=> x a [/= b [[/=c openc] cb bx ba]]. rewrite /nbhs/= /filter_from/=. diff --git a/theories/numfun.v b/theories/numfun.v index 534f7ce698..f6e49c46b8 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1146,10 +1146,10 @@ by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n. Unshelve. all: by end_near. Qed. (* NB: should appear in MathComp 2.6.0 (PR #1586) *) -Notation "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]" := - (GRing.SubZmodule_isSubPzRing.Build _ _ U (subringClosedP _)) +(*Notation "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]" := + (GRing.SubNmodule_isSubPzSemiRing.Build _ _ U (subringClosedP _)) (format "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]") - : form_scope. + : form_scope.*) Section ring. Context (aT : Type) (rT : pzRingType). @@ -1162,7 +1162,7 @@ Qed. HB.instance Definition _ := @GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed. -HB.instance Definition _ := [SubZmodule_isSubPzRing of {fimfun aT >-> rT} by <:]. +HB.instance Definition _ := [SubNmodule_isSubPzSemiRing of {fimfun aT >-> rT} by <:]. Implicit Types f g : {fimfun aT >-> rT}. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 7ca2cba748..2ab9993826 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_ssreflect_compat algebra. From mathcomp Require Import interval_inference. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index 6bae7eea60..8c734a6876 100644 --- a/theories/topology_theory/bool_topology.v +++ b/theories/topology_theory/bool_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology compact. From mathcomp Require Import discrete_topology. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index cbe8001938..6775a6058d 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index b67a9cc0e9..333150b1b3 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 72bd27fbdc..3476d4b561 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -1,5 +1,6 @@ +(* 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 all_reals. +From mathcomp Require Import all_ssreflect_compat algebra all_classical all_reals. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import order_topology pseudometric_structure compact. diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index dee7ebdac1..40dbfdc307 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import generic_quotient. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. @@ -437,8 +437,8 @@ Proof. exact: nbhs_pfilter. Qed. End product_spaces. -HB.instance Definition _ (U : Type) (T : U -> ptopologicalType) := - Pointed.copy (forall x : U, T x) (prod_topology T). +(*HB.instance Definition _ (U : Type) (T : U -> ptopologicalType) := + Pointed.copy (forall x : U, T x) (prod_topology T).*) (**md the uniform topologies type *) Section fct_Uniform. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index f0d861df4d..943c1210cb 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. @@ -55,18 +55,18 @@ Section Initial_Topology. Variable (S : choiceType) (T : topologicalType) (f : S -> T). Local Notation W := (initial_topology f). -Definition wopen := [set f @^-1` A | A in open]. +Definition initial_open := [set f @^-1` A | A in open]. -Local Lemma wopT : wopen [set: W]. -Proof. by exists setT => //; apply: openT. Qed. +Let initial_opT : initial_open [set: W]. +Proof. by exists setT => //; exact: openT. Qed. -Local Lemma wopI : setI_closed wopen. +Let initial_opI : setI_closed initial_open. Proof. by move=> ? ? [C Cop <-] [D Dop <-]; exists (C `&` D) => //; exact: openI. Qed. -Local Lemma wop_bigU (I : Type) (g : I -> set W) : - (forall i, wopen (g i)) -> wopen (\bigcup_i g i). +Let initial_op_bigU (I : Type) (g : I -> set W) : + (forall i, initial_open (g i)) -> initial_open (\bigcup_i g i). Proof. move=> gop. set opi := fun i => [set Ui | open Ui /\ g i = f @^-1` Ui]. @@ -81,7 +81,7 @@ Qed. HB.instance Definition _ := Choice.on W. HB.instance Definition _ := - isOpenTopological.Build W wopT wopI wop_bigU. + isOpenTopological.Build W initial_opT initial_opI initial_op_bigU. Lemma initial_continuous : continuous (f : W -> T). Proof. by apply/continuousP => A ?; exists A. Qed. @@ -102,6 +102,8 @@ by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. End Initial_Topology. +(*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")] +Notation wopen := initial_open (only parsing).*) HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) := Pointed.on (initial_topology f). diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index 33334d0359..545a8fc5cb 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -1,6 +1,6 @@ (* 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 all_classical. +From mathcomp Require Import all_ssreflect_compat algebra finmap all_classical. From mathcomp Require Import interval_inference topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index ec29a30b3f..e2d0274f38 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 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 all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import reals topology_structure uniform_structure. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 9c90ac5101..fc7caea215 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. From mathcomp Require Import order_topology matrix_topology. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index cc082f9b19..3eb6674e66 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure compact initial_topology. diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 7327a69d93..314fe8952e 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -1,6 +1,6 @@ (* 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 all_classical. +From mathcomp Require Import all_ssreflect_compat algebra finmap all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import topology_structure uniform_structure. diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 96d2acaf9e..da78449139 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference topology_structure. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index 172c467876..ef04f0560f 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure. diff --git a/theories/topology_theory/quotient_topology.v b/theories/topology_theory/quotient_topology.v index d322b01160..1a0ac8a22f 100644 --- a/theories/topology_theory/quotient_topology.v +++ b/theories/topology_theory/quotient_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index e03450bb79..5965dcb7a8 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality fsbigop. From mathcomp Require Import set_interval filter reals interval_inference. diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v index d5eda111ef..049bbcbb31 100644 --- a/theories/topology_theory/sigT_topology.v +++ b/theories/topology_theory/sigT_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import topology_structure compact subspace_topology. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index efab8ebfe2..3071877d51 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import topology_structure uniform_structure compact. From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology. diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index e194598ad5..e5a025e01b 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/theories/topology_theory/subtype_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import reals topology_structure uniform_structure compact. From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology subspace_topology. diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v index 33b699bd9d..72d89a081a 100644 --- a/theories/topology_theory/supremum_topology.v +++ b/theories/topology_theory/supremum_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat algebra finmap all_classical. From mathcomp Require Import topology_structure uniform_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 1006a5edfd..9ba7b9cfa5 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -1,6 +1,6 @@ (* 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. +From mathcomp Require Import all_ssreflect_compat algebra finmap. From mathcomp Require Import all_classical. From mathcomp Require Export filter. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 8df9557bcd..44e5ce8742 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 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 all_ssreflect_compat algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 667e33095f..fc519bffcc 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -1,6 +1,6 @@ (* 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 all_ssreflect_compat algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure.