replace a lemma by its near version

Co-authored-by: zstone1 <[email protected]>

theories/lebesgue_measure.v

@@ -2348,10 +2348,15 @@ have ZNF5 : Z r%:num `<=`
     case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz.
     have [d dzr zdK0] : exists2 d : {posnum R},
         (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0.
-      move: rz; rewrite -subr_gt0.
-      move=> /(@closed_disjoint_closed_ball _ [normedModType R of R^o]
-                                            _ _ _ closedK Kz).
-      by case=> d drz zdK; exists d.
+      have [d/= d0 dzK] := (@closed_disjoint_closed_ball _
+        [normedModType R of R^o] _ _ closedK Kz).
+      have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R.
+        by rewrite lt_minr (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
+      exists (PosNum rz0) => /=.
+        by rewrite lt_minl ltr_pdivr_mulr// ltr_pmulr ?subr_gt0// ltr1n.
+      apply: dzK => //=.
+      rewrite sub0r normrN gtr0_norm// lt_minl (ltr_pdivr_mulr d d)//.
+      by rewrite ltr_pmulr// ltr1n orbT.
     have N0_gt0 : (0 < d%:num / 2 :> R)%R by rewrite divr_gt0.
     have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0.
     exists i; split => //.

theories/normedtype.v

@@ -5916,38 +5916,28 @@ Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V)
   (r : R) : ball x r `<=` closed_ball x r.
 Proof. exact: subset_closure. Qed.
 
-Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M) (x : M)
-    k : open A -> A x -> 0 < k ->
-  exists2 e : {posnum R}, e%:num < k & ball x e%:num `<=` A.
-Proof.
-move=> aA Ax k0; have : nbhs x A by rewrite nbhsE/=; exists A.
-move/(@nbhs_closedballP R M _ x) => [r xrA].
-have r2k20 : 0 < minr (r%:num / 2) (k / 2) by rewrite lt_minr// !divr_gt0.
-exists (PosNum r2k20) => /=.
-  by rewrite lt_minl orbC ltr_pdivr_mulr// ltr_pmulr// ltr1n.
+Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M)
+    (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
+Proof.
+move=> aA Ax.
+have /(@nbhs_closedballP R M _ x)[r xrA]: nbhs x A by rewrite nbhsE/=; exists A.
+near=> e.
 apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //.
-by apply: le_ball; rewrite le_minl; rewrite ler_pdivr_mulr// ler_pmulr// ler1n.
-Qed.
+by apply: le_ball; near: e; apply: nbhs_right_le.
+Unshelve. all: by end_near. Qed.
 
 Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R}
-    (K : set M) z (k : R) : closed K -> ~ K z -> 0 < k ->
-  exists2 d : {posnum R}, d%:num < k & closed_ball z d%:num `&` K = set0.
-Proof.
-move=> cK Kz k0.
-have [e ek zeK] : exists2 e : {posnum R}, e%:num < k & ball z e%:num `<=` ~` K.
-  by apply: open_subball => //; rewrite openC.
-have e20 : 0 < e%:num / 2 by rewrite divr_gt0.
-have e2e : e%:num / 2 < e%:num by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n.
-exists (e%:num / 2)%:pos; first by rewrite /= (lt_trans _ ek).
-move/subsets_disjoint : zeK; rewrite setCK.
-apply: subsetI_eq0 => //=.
-have := @closed_ball_subset _ M z _ _ e20 e2e.
-by rewrite closed_ballE.
-Qed.
-(*NB: make it a near lemma?
-  Lemma near_closed_disjoint_closed_ball {R : realType} {X : pseudoMetricType R}
-    (K : set X) z : closed K -> ~ K z ->
-  \forall d \near 0^'+, closed_ball z d `&` K = set0.*)
+    (K : set M) z : closed K -> ~ K z ->
+  \forall d \near 0^'+, closed_ball z d `&` K = set0.
+Proof.
+rewrite -openC => /open_subball /[apply]; move=> [e /= e0].
+move=> /(_ (e / 2)) /= ; rewrite sub0r normrN gtr0_norm ?divr_gt0//.
+rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n => /(_ erefl isT).
+move/subsets_disjoint; rewrite setCK => ze2K0.
+exists (e / 2); first by rewrite /= divr_gt0.
+move=> x /= + x0; rewrite sub0r normrN gtr0_norm// => xe.
+by move: ze2K0; apply: subsetI_eq0 => //=; exact: closed_ball_subset.
+Qed.
 
 Lemma locally_compactR (R : realType) : locally_compact [set: R].
 Proof.
@@ -5957,7 +5947,7 @@ by split; [apply: closed_ballR_compact | apply: closed_ball_closed].
 Qed.
 
 Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V)
-  (r : R) : 0 < r -> closed_ball x (r/2) `<=` ball x r.
+  (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r.
 Proof.
 move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) [].
   exact: nbhsx_ballx.