Fixes 1042, 1037, 1045, 1046

CHANGELOG_UNRELEASED.md

@@ -4,12 +4,21 @@
 
 ### Added
 
+- in `constructive_ereal.v`:
+  + lemmas `gt0_fin_numE`, `lt0_fin_numE`
+
 ### Changed
 
+- in `hoelder.v`:
+  + definition `Lnorm` now `HB.lock`ed
+
 ### Renamed
 
 ### Generalized
 
+- in `topology.v`:
+  + `ball_filter` generalized to `realDomainType`
+
 ### Deprecated
 
 ### Removed

theories/charge.v

@@ -471,8 +471,7 @@ have := d_ge0 A; rewrite le_eqVlt => /predU1P[<-|d_gt0].
 have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A.
   rewrite /m; have [->|dn1oo] := eqVneq (d_ A) +oo.
     by rewrite min_r ?ltey ?gt0_mulye ?leey.
-  rewrite -(@fineK _ (d_ A)); last first.
-    by rewrite ge0_fin_numE// ?(ltW d_gt0)// lt_neqAle dn1oo leey.
+  rewrite -(@fineK _ (d_ A)); last by rewrite gt0_fin_numE// ltey.
   rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left.
   by rewrite ltr_pdivr_mulr// ltr_pmulr ?ltr1n// fine_gt0// d_gt0/= ltey.
 by exists B; split => //; rewrite (le_trans _ (ltW mnuB)).
@@ -649,8 +648,7 @@ have := s_le0 U; rewrite le_eqVlt => /predU1P[->|s_lt0].
 have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m.
   rewrite /m; have [->|s0oo] := eqVneq (s_ U) -oo.
     by rewrite max_r ?ltNye// gt0_mulNye// leNye.
-  rewrite -(@fineK _ (s_ U)); last first.
-    by rewrite le0_fin_numE// ?(ltW s_lt0)// lt_neqAle leNye eq_sym s0oo.
+  rewrite -(@fineK _ (s_ U)); last by rewrite lt0_fin_numE// ltNye.
   rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left.
   by rewrite ltr_pdivl_mulr// gtr_nmulr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT.
 have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB.

theories/constructive_ereal.v

@@ -1468,9 +1468,15 @@ Proof. by case: x => // x //=; exact: ltNyr. Qed.
 Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo).
 Proof. by move: x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed.
 
+Lemma gt0_fin_numE x : 0 < x -> (x \is a fin_num) = (x < +oo).
+Proof. by move/ltW; exact: ge0_fin_numE. Qed.
+
 Lemma le0_fin_numE x : x <= 0 -> (x \is a fin_num) = (-oo < x).
 Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.
 
+Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x).
+Proof. by move/ltW; exact: le0_fin_numE. Qed.
+
 Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x).
 Proof.
 split=> [-> // A A0|Ax]; first by rewrite leey.

theories/hoelder.v

@@ -37,13 +37,8 @@ Declare Scope Lnorm_scope.
 
 Local Open Scope ereal_scope.
 
-Section Lnorm.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Local Open Scope ereal_scope.
-Implicit Types (p : \bar R) (f g : T -> R) (r : R).
-
-Definition Lnorm p f :=
+HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
+    (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
   match p with
   | p%:E => if p == 0%R then
               mu (f @^-1` (setT `\ 0%R))
@@ -52,19 +47,27 @@ Definition Lnorm p f :=
   | +oo => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0
   | -oo => 0
   end.
+Canonical locked_Lnorm := Unlockable Lnorm.unlock.
+Arguments Lnorm {d T R} mu p f.
 
-Local Notation "'N_ p [ f ]" := (Lnorm p f).
+Section Lnorm_properties.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+Implicit Types (p : \bar R) (f g : T -> R) (r : R).
+
+Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
 
 Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
 Proof.
-rewrite /Lnorm oner_eq0 invr1// poweRe1//.
+rewrite unlock oner_eq0 invr1// poweRe1//.
   by apply: eq_integral => t _; rewrite powRr1.
 by apply: integral_ge0 => t _; rewrite powRr1.
 Qed.
 
 Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
 Proof.
-move: p => [r/=|/=|//].
+rewrite unlock; move: p => [r/=|/=|//].
   by case: ifPn => // r0; exact: poweR_ge0.
 by case: ifPn => // /ess_sup_ge0; apply => t/=.
 Qed.
@@ -75,7 +78,7 @@ Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
 Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f ->
   'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0).
 Proof.
-move=> r0 mf/=; rewrite (gt_eqF r0) => /poweR_eq0_eq0 fp.
+move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp.
 apply/ae_eq_integral_abs => //=.
   apply: measurableT_comp => //.
   apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
@@ -84,22 +87,22 @@ under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
 by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
 Qed.
 
-End Lnorm.
+End Lnorm_properties.
 #[global]
 Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
 
 Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
 
 Section lnorm.
-(* lnorm is just Lnorm applied to counting *)
+(* l-norm is just L-norm applied to counting *)
 Context d {T : measurableType d} {R : realType}.
 
 Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f).
 
 Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
   'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
 Proof.
-move=> p0 /=; rewrite gt_eqF// ge0_integral_count// => k.
+move=> p0; rewrite unlock gt_eqF// ge0_integral_count// => k.
 by rewrite lee_fin powR_ge0.
 Qed.
 
@@ -118,28 +121,26 @@ Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
 Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
 
 Let integrable_powR f p : (0 < p)%R ->
-  measurable_fun [set: T] f -> 'N_p%:E[f] != +oo ->
+    measurable_fun [set: T] f -> 'N_p%:E[f] != +oo ->
   mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
 Proof.
 move=> p0 mf foo; apply/integrableP; split.
   apply: measurableT_comp => //; apply: measurableT_comp_powR.
   exact: measurableT_comp.
 rewrite ltey; apply: contra foo.
 move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-.
-rewrite /= (gt_eqF p0); apply/eqP; congr (_ `^ _).
-by apply/eq_integral => t _; rewrite ger0_norm// powR_ge0.
+rewrite unlock (gt_eqF p0); apply/eqP; congr (_ `^ _).
+by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0.
 Qed.
 
 Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g ->
-  (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
+    (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
   'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R]  <= 'N_p%:E[f] * 'N_q%:E[g].
 Proof.
 move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//.
 rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
-- apply: measurableT_comp => //; apply: measurableT_comp => //.
-  exact: measurable_funM.
-- have := Lnorm_eq0_eq0 p0 mf f0.
-  apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _.
+- by do 2 apply: measurableT_comp => //; exact: measurable_funM.
+- apply: filterS (Lnorm_eq0_eq0 p0 mf f0) => x /(_ I)[] /powR_eq0_eq0 + _.
   by rewrite normrM => ->; rewrite mul0r.
 Qed.
 
@@ -153,7 +154,7 @@ Let measurable_normalized p f : measurable_fun [set: T] f ->
 Proof. by move=> mf; apply: measurable_funM => //; exact: measurableT_comp. Qed.
 
 Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] ->
-  mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
+    mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
   \int[mu]_x (normalized p f x `^ p)%:E = 1.
 Proof.
 move=> p0 fpos ifp.
@@ -163,21 +164,21 @@ transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E).
   rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
   by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
 have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E.
-  rewrite /= (gt_eqF p0) in fpos.
+  rewrite unlock (gt_eqF p0) in fpos.
   apply: gt0_poweR fpos; rewrite ?invr_gt0//.
   by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
-rewrite /Lnorm (gt_eqF p0) -poweRrM mulVf ?lt0r_neq0// poweRe1//; last exact: ltW.
+rewrite unlock (gt_eqF p0) -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//.
 under eq_integral do rewrite EFinM muleC.
 have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
   move/integrableP: ifp => -[_].
   by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
 rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1.
-- by rewrite fineK// ge0_fin_numE// ltW.
+- by rewrite fineK// gt0_fin_numE.
 - by rewrite gt_eqF// fine_gt0// foo andbT.
 Qed.
 
 Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g ->
-  (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
+    (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
  'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
 Proof.
 move=> mf mg p0 q0 pq.
@@ -199,9 +200,8 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
       by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
     by rewrite mulrC -normrM EFinM; over.
   rewrite ge0_integralZl//; last 2 first.
-    - apply: measurableT_comp => //; apply: measurableT_comp => //.
-      exact: measurable_funM.
-    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0//Lnorm_ge0.
+    - by do 2 apply: measurableT_comp => //; exact: measurable_funM.
+    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
   rewrite -muleA muleC muleA EFinM muleCA 2!muleA.
   rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
     rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
@@ -212,7 +212,7 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
 rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
 rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
   rewrite Lnorm1 ae_ge0_le_integral //.
-  - apply: measurableT_comp => //; apply: measurableT_comp => //.
+  - do 2 apply: measurableT_comp => //.
     by apply: measurable_funM => //; exact: measurable_normalized.
   - by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW.
   - by apply: measurableT_comp => //; apply: measurable_funD => //;
@@ -223,10 +223,10 @@ rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
 under eq_integral do rewrite EFinD mulrC (mulrC _ (_^-1)).
 rewrite ge0_integralD//; last 4 first.
 - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
-- apply: measurableT_comp => //; apply: measurableT_comp => //.
+- do 2 apply: measurableT_comp => //.
   by apply: measurableT_comp_powR => //; exact: measurable_normalized.
 - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
-- apply: measurableT_comp => //; apply: measurableT_comp => //.
+- do 2 apply: measurableT_comp => //.
   by apply: measurableT_comp_powR => //; exact: measurable_normalized.
 under eq_integral do rewrite EFinM.
 rewrite {1}ge0_integralZl//; last 3 first.

theories/lebesgue_integral.v

@@ -1090,8 +1090,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
   by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n.
 have := leey (\int[mu]_x (f x)).
 rewrite le_eqVlt => /predU1P[|] mufoo; last first.
-  have : \int[mu]_x (f x) \is a fin_num.
-    by rewrite ge0_fin_numE//; exact: integral_ge0.
+  have : \int[mu]_x (f x) \is a fin_num by rewrite ge0_fin_numE// integral_ge0.
   rewrite ge0_integralTE// => /ub_ereal_sup_adherent h.
   apply/lee_addgt0Pr => _/posnumP[e].
   have {h} [/= _ [G Gf <-]] := h _ [gt0 of e%:num].
@@ -1275,7 +1274,7 @@ Let fpos_approx_neq0 x : D x -> (0%E < f x < +oo)%E ->
   \forall n \near \oo, approx n x != 0.
 Proof.
 move=> Dx /andP[fx_gt0 fxoo].
-have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// ltW.
+have fxfin : f x \is a fin_num by rewrite gt0_fin_numE.
 rewrite -(fineK fxfin) lte_fin in fx_gt0; near=> n.
 rewrite /approx paddr_eq0//; last 2 first.
   by apply: sumr_ge0 => i _; rewrite mulr_ge0.
@@ -1421,7 +1420,7 @@ have cvg_af := cvg_approx fi0 Dx fixoo.
 have is_cvg_af : cvg (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af.
 have {is_cvg_af} := nondecreasing_cvg_le nd_ag is_cvg_af k.
 rewrite -lee_fin => /le_trans; apply.
-rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE //; apply: f0.
+rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0.
 by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->.
 Qed.
 
@@ -1720,7 +1719,7 @@ move=> D [/= mD Deps KDf]; exists (K `\` D); split => //.
     by apply: measureU2 => //; apply: measurableI => //; apply: measurableC.
   rewrite [_%:num]splitr EFinD; apply: lee_lt_add => //=; first 2 last.
   + by rewrite (@le_lt_trans _ _ (mu D)) ?le_measure ?inE//; exact: measurableI.
-  + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure// ?inE//.
+  + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure ?inE//.
     exact: measurableD.
   rewrite setDE setC_bigcap setI_bigcupr.
   apply: (@le_trans _ _(\sum_(k <oo) mu (A `\` gK k))).
@@ -2450,10 +2449,9 @@ rewrite monotone_convergence //.
     exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
   exists `|ceil (M / fine (mu D))|%N => // m /=.
-  rewrite -(ler_nat R) => MDm.
-  rewrite -(@fineK _ (mu D)); last by rewrite ge0_fin_numE.
+  rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
-  rewrite lee_fin; apply: le_trans MDm.
+  rewrite lee_fin (le_trans _ MDm)//.
   by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm.
 - by move=> n; exact: measurable_cst.
 - by move=> n x Dx; rewrite lee_fin.
@@ -3211,7 +3209,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
     - by move=> *; rewrite lee_fin.
   rewrite fineK//; last first.
     case: (integrableP _ _ _ fint) => _ foo.
-    by rewrite ge0_fin_numE//; exact: integral_ge0.
+    by rewrite ge0_fin_numE// integral_ge0.
   apply: ge0_le_integral => //.
   - by move=> *; rewrite lee_fin /indic.
   - exact/EFin_measurable_fun/measurableT_comp.
@@ -3303,7 +3301,7 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
       \int[mu]_(x in D) (g1^\+ x) + \int[mu]_(x in D) (g2^\+ x) \is a fin_num.
     rewrite ge0_fin_numE//.
       by rewrite lte_add_pinfty//; exact: integral_funepos_lt_pinfty.
-    by apply: adde_ge0; exact: integral_ge0.
+    by rewrite adde_ge0// integral_ge0.
   have g12neg :
       \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) \is a fin_num.
     rewrite ge0_fin_numE//.
@@ -3313,9 +3311,8 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
     - rewrite ge0_fin_numE.
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
-        have : mu.-integrable D (g1 \+ g2) by apply: integrableD.
-        exact: integral_funepos_lt_pinfty.
-      apply: adde_ge0; last exact: integral_ge0.
+        exact: integral_funepos_lt_pinfty (integrableD _ _ _).
+      rewrite adde_ge0//; last exact: integral_ge0.
       by apply: adde_ge0; exact: integral_ge0.
     - by rewrite fin_num_adde_defr.
   rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)).
@@ -4548,8 +4545,7 @@ have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E.
   exists (fine (m2Fn (F n)) + 1) => Y mY.
   rewrite [in ltRHS]EFinD lte_spadder// fineK; last first.
     by rewrite ge0_fin_numE ?measure_ge0//= /mrestr/= setIid.
-  rewrite /= /mrestr/= setIid; apply: le_measure => //; rewrite inE//.
-  exact: measurableI.
+  by rewrite /= /mrestr/= setIid le_measure// inE//; exact: measurableI.
 pose phi' A := m2Fn \o xsection A.
 pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)].
 have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection.
@@ -4584,8 +4580,7 @@ have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E.
   exists (fine (m1Fn (F n)) + 1) => Y mY.
   rewrite [in ltRHS]EFinD lte_spadder// fineK; last first.
     by rewrite ge0_fin_numE ?measure_ge0// /m1Fn/= /mrestr setIid.
-  rewrite /m1Fn/= /mrestr setIid; apply: le_measure => //; rewrite inE//=.
-  exact: measurableI.
+  by rewrite /m1Fn/= /mrestr setIid le_measure// inE//=; exact: measurableI.
 pose psi' A := m1Fn \o ysection A.
 pose B' := [set A | measurable A /\ measurable_fun setT (psi' A)].
 have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection.
@@ -5548,7 +5543,7 @@ Qed.
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
 
-Section lebesgue_differentiation.
+Section lebesgue_differentiation_continuous.
 Context (rT : realType).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
 Let R  := [the measurableType _ of measurableTypeR rT].
@@ -5631,4 +5626,4 @@ apply: le_trans.
 by rewrite ritv //= -EFinM lee_fin mulrC.
 Unshelve. all: by end_near. Qed.
 
-End lebesgue_differentiation.
+End lebesgue_differentiation_continuous.

theories/measure.v

@@ -2975,7 +2975,7 @@ Let mnormalize1 : mnormalize [set: T] = 1.
 Proof.
 rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
 rewrite negb_or => /andP[ft0 ftoo].
-have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey.
+have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey.
 by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0.
 Qed.
 

theories/normedtype.v

@@ -3795,7 +3795,7 @@ Qed.
 Lemma edist_pinfty_open : open [set xy : X * X | edist xy = +oo]%E.
 Proof.
 rewrite -closedC; have := edist_fin_closed; congr (_ _).
-by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE // ltey; move/eqP.
+by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE// ltey => /eqP.
 Qed.
 
 Lemma edist_sym (x y : X) : edist (x, y) = edist (y, x).
@@ -4034,11 +4034,11 @@ Section topological_urysohn_separator.
 Context {T : topologicalType} {R : realType}.
 
 Definition uniform_separator (A B : set T) :=
-  exists (uT : @Uniform.class_of T^o) (E : set (T * T)), 
-    let UT := Uniform.Pack uT in [/\ 
+  exists (uT : @Uniform.class_of T^o) (E : set (T * T)),
+    let UT := Uniform.Pack uT in [/\
       @entourage UT E, A `*` B `&` E = set0 &
       (forall x, @nbhs UT UT x `<=` @nbhs T T x)].
-    
+
 Local Lemma Urysohn' (A B : set T) : exists (f : T -> R),
     [/\ continuous f,
     range f `<=` `[0, 1]