diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b4fcf9213..ea9c36400 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/cardinality.v b/classical/cardinality.v index ba1e49275..7afaef4ee 100644 --- a/classical/cardinality.v +++ b/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. diff --git a/classical/unstable.v b/classical/unstable.v index 6fb3c6cf6..b12853ecc 100644 --- a/classical/unstable.v +++ b/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,9 +387,11 @@ 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. @@ -398,6 +399,7 @@ 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. diff --git a/coq-mathcomp-analysis-stdlib.opam b/coq-mathcomp-analysis-stdlib.opam index ef8ac571e..1abd3d74a 100644 --- a/coq-mathcomp-analysis-stdlib.opam +++ b/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" diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index e938cb24a..41d08d317 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/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 *) diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 272bcbc67..575beac12 100644 --- a/theories/topology_theory/order_topology.v +++ b/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 *) (* ``` *) (******************************************************************************)