Merge pull request #1815 from affeldt-aist/normed_module_20260101

various easy issues

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -106,6 +106,9 @@
 
 - in `lebesgue_integrable.v`:
   + lemma `integrable_norm`
+- in `order_topology.v`:
+  + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`,
+    `POrderedPointedTopological`
 
 ### Changed
 

classical/cardinality.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 finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
@@ -430,7 +430,7 @@ Qed.
 Lemma card_eq_II {n m} : reflect (n = m) (`I_n #= `I_m).
 Proof. by rewrite card_eq_le !card_le_II -eqn_leq; apply: eqP. Qed.
 
-Lemma sub_setP  {T} {A : set T} (X : set A) : set_val @` X `<=` A.
+Lemma sub_setP {T} {A : set T} (X : set A) : set_val @` X `<=` A.
 Proof. by move=> x [/= a Xa <-]; apply: set_valP. Qed.
 Arguments sub_setP {T A}.
 Arguments image_subset {aT rT} f [A B].
@@ -444,7 +444,7 @@ exists (set_val @` range f); last exact: (subset_trans (sub_setP _)).
 by rewrite ?(card_eql (inj_card_eq _))//; apply: in2W; apply: in2TT; apply: inj.
 Qed.
 
-(* remove *)
+#[deprecated(since="mathcomp-analysis 1.15.0", note="To be removed, use other lemmas instead.")]
 Lemma pigeonhole m n (f : nat -> nat) : {in `I_m &, injective f} ->
   f @` `I_m `<=` `I_n -> (m <= n)%N.
 Proof.

classical/unstable.v

@@ -229,8 +229,7 @@ Inductive boxed T := Box of T.
 Reserved Notation "`1- r" (format "`1- r", at level 2).
 Reserved Notation "f \^-1" (at level 35, format "f \^-1").
 
-(* TODO: To be backported to finmap *)
-
+(* PR in progress: https://github.com/math-comp/finmap/pull/149 *)
 Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
     (f : X -> nat) : A != fset0 ->
   (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat.
@@ -388,16 +387,19 @@ Qed.
 
 End order_min.
 
+(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
 Lemma intrD1 {R : pzRingType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
 Proof. by rewrite intrD. Qed.
 
+(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
 Lemma intr1D {R : pzRingType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
 Proof. by rewrite intrD. Qed.
 
 Section trunc_floor_ceil.
 Context {R : archiRealDomainType}.
 Implicit Type x : R.
 
+(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
 Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
 Proof.
 rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.

coq-mathcomp-analysis-stdlib.opam

@@ -21,6 +21,7 @@ depends: [
 
 tags: [
   "category:Mathematics/Real Numbers"
+  "category:Mathematics/Real Calculus and Topology"
   "keyword:real numbers"
   "keyword:reals"
   "logpath:mathcomp.reals_stdlib"

theories/normedtype_theory/normed_module.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 finmap ssralg ssrnum ssrint.
 From mathcomp Require Import archimedean rat interval zmodp vector.
@@ -43,6 +43,7 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 (*                  lipschitz_on f F == f is lipschitz near F                 *)
 (*               k.-lipschitz_on f F == f is k.-lipschitz near F              *)
 (*                  k.-lipschitz_A f == f is k.-lipschitz on A                *)
+(*                    k.-lipschitz f := k.-lipschitz_setT                     *)
 (*          [lipschitz f x | x in A] == f is lipschitz on A                   *)
 (* [locally [lipschitz f x | x in A] == f is locally lipschitz on A           *)
 (*        [locally k.-lipschitz_A f] == f is locally k.-lipschitz on A        *)

theories/topology_theory/order_topology.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 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 all_algebra finmap all_classical.
 From mathcomp Require Import unstable topology_structure uniform_structure.
@@ -8,8 +8,13 @@ From mathcomp Require Import product_topology pseudometric_structure.
 (* # Order topology                                                           *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*             orderTopologicalType == a topology built from intervals        *)
-(*                 order_topology T == the induced order topology on T        *)
+(*                    POrderedNbhs == join of Nbhs and isPOrder               *)
+(*             POrderedTopological == join of Topological and isPOrder        *)
+(*                 POrderedUniform == join of Uniform and isPOrder            *)
+(*            POrderedPseudoMetric == join of PseudoMetric and isPOrder       *)
+(*      POrderedPointedTopological == join of PointedTopological and isPOrder *)
+(*            orderTopologicalType == a topology built from intervals         *)
+(*                order_topology T == the induced order topology on T         *)
 (* ```                                                                        *)
 (******************************************************************************)