Fixes 1931 (#1932)

* fixes #1931

* fixes #1930

Author: affeldt-aist

theories/normedtype_theory/normed_module.v

@@ -1040,11 +1040,11 @@ split=> [Ea V aV|]; last first.
 pose elt_prop (ar : R * R) := [/\ ball a ar.2 `<=` V,
   ar.1 \in E, ar.1 \in (ball a ar.2 : set R), ar.2 > 0 & ar.1 != a].
 pose elt_type := {ar : R * R | elt_prop ar}.
-pose a_ (x : elt_type) := (proj1_sig x).2.
-pose r_ (x : elt_type) := (proj1_sig x).1.
+pose a_ (x : elt_type) := (proj1_sig x).1.
+pose r_ (x : elt_type) := (proj1_sig x).2.
 (* two successive (a_i, r_i) and (a_j, r_j) satisfy the relation: *)
-pose elt_rel i j := `|a - r_ i| = a_ j /\ ball a (a_ j) `<=` ball a (a_ i) /\
-  `|a - r_ j| < `|a - r_ i| /\ r_ i != r_ j.
+pose elt_rel i j := `|a - a_ i| = r_ j /\ ball a (r_ j) `<=` ball a (r_ i) /\
+  `|a - a_ j| < `|a - a_ i| /\ a_ i != a_ j.
 move: aV => -[r0/= r0_gt0 ar0V].
 pose V0 : set R := ball a r0.
 move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
@@ -1056,7 +1056,7 @@ have [a0 [a0a a0V0 a0E]] : exists a0, [/\ a0 != a, a0 \in V0 & a0 \in E].
 have [v [v0 Pv]] : {v : nat -> elt_type |
     v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
     forall n, elt_rel (v n) (v n.+1)}.
-  apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
+apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
   pose rj : R := `|a - ai|.
   have rj_gt0 : 0 < rj by rewrite /rj normr_gt0 subr_eq0 eq_sym.
   apply/cid; move/cvgrPdist_lt : y_cvg_a => /(_ _ rj_gt0)[M/= _ May_rj].
@@ -1070,14 +1070,14 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
   have y_ME : y_ M \in E by rewrite inE; apply/y_E/imageT.
   exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.
   split; first exact.
-  split; rewrite /a_ /r_/=.
+  split; rewrite /r_ /a_/=.
     by apply: le_ball; move: aiari; rewrite inE => /ltW.
   split; first by move: y_MVj; rewrite inE.
   by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
-apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).
-  move=> n _; rewrite /r_ /=.
+apply/infiniteP/pcard_leP/injfunPex => /=; exists (a_ \o v).
+  move=> n _; rewrite /a_ /=.
   by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
-have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
+have arv q p : (p < q)%N -> `|a - a_ (v q)| < `|a - a_ (v p)|.
   elim: q p => [[]//|q ih p].
   by rewrite ltnS leq_eqVlt => /predU1P[->|/ih]; last apply: lt_trans;
     by case: (Pv q) => _ [] _ [].

theories/topology_theory/topology_structure.v

@@ -791,7 +791,7 @@ Lemma closed_closure (A : set T) : closed (closure A).
 Proof. by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed.
 
 End Closed.
-#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_limit_point_isolated` instead")]
+#[deprecated(since="mathcomp-analysis 1.15.0", note="use `closure_isolated_limit_point` instead")]
 Notation closure_limit_point := __deprecated__closure_limit_point (only parsing).
 
 Lemma preimage_closed {T U : topologicalType} (f : T -> U) (D : set U) :