Fixes 20231117 (math-comp#1106)

* fixes math-comp#1104 * fixes math-comp#1103 * fixes math-comp#1099 * fixes math-comp#1098 * fixes math-comp#1093
affeldt-aist · Dec 7, 2023 · 1b4404e · 1b4404e
1 parent 480ca05
commit 1b4404e
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 7 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -26,6 +26,9 @@
 
 ### Renamed
 
+- in `exp.v`:
+  + `lnX` -> `lnXn`
+
 ### Generalized
 
 ### Deprecated

diff --git a/theories/Make b/theories/Make
@@ -13,6 +13,7 @@ reals.v
 landau.v
 Rstruct.v
 topology.v
+cantor.v
 prodnormedzmodule.v
 normedtype.v
 realfun.v

diff --git a/theories/cantor.v b/theories/cantor.v
@@ -1,8 +1,9 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
-From mathcomp Require Import interval rat fintype finmap.
-Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
-Require Import reals topology.
+From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
+From mathcomp Require Import finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
+Require Import reals signed topology.
 From HB Require Import structures.
 
 (******************************************************************************)

diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
@@ -624,7 +624,7 @@ Context {R : numDomainType}.
 Implicit Type (x : \bar R).
 
 Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
-Fact fin_num_key : pred_key fin_num. by []. Qed.
+Fact fin_num_key : pred_key fin_num. Proof. by []. Qed.
 Canonical fin_num_keyd := KeyedQualifier fin_num_key.
 
 Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).

diff --git a/theories/exp.v b/theories/exp.v
@@ -631,7 +631,7 @@ Proof. by move=> x y x_gt0 y_gt0; rewrite -ltr_expR !lnK. Qed.
 Lemma ler_ln : {in Num.pos &, {mono ln : x y / x <= y}}.
 Proof. by move=> x y x_gt0 y_gt0; rewrite -ler_expR !lnK. Qed.
 
-Lemma lnX n x : 0 < x -> ln(x ^+ n) = ln x *+ n.
+Lemma lnXn n x : 0 < x -> ln (x ^+ n) = ln x *+ n.
 Proof.
 move=> x_gt0; elim: n => [|n ih] /=; first by rewrite expr0 ln1 mulr0n.
 by rewrite !exprS lnM ?qualifE//= ?exprn_gt0// mulrS ih.

diff --git a/theories/topology.v b/theories/topology.v
@@ -2520,7 +2520,7 @@ HB.instance Definition _ :=
 
 End Product_Topology.
 
-(** dnbhs *)
+(** deleted neighborhood *)
 
 Definition dnbhs {T : topologicalType} (x : T) :=
   within (fun y => y != x) (nbhs x).