small lint

math-comp · Aug 5, 2023 · 7d2f2b4 · 7d2f2b4
1 parent 8d47d78
commit 7d2f2b4
Showing 1 changed file with 19 additions and 16 deletions.
diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -4188,6 +4188,8 @@ exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split.
 Qed.
 
 Section normalP.
+Locate Real.type.
+Print realType.
 Context {T : topologicalType} {R : realType}.
 Let normal_spaceP : [<->
 (* 0 *) normal_space T;
@@ -4197,12 +4199,12 @@ Let normal_spaceP : [<->
   exists U V, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0]
 ].
 Proof.
-tfae; first by move=> *; exact: normal_uniform_separator.
+tfae; first by move=> ?; exact: normal_uniform_separator.
 - move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R).
-  case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1]. 
+  case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1].
   exists (f@^-1` `]-1, 1/2[), (f@^-1` `]1/2, 2[); split.
-  + by apply: open_comp; [|exact: interval_open] => + _ .
-  + by apply: open_comp; [|exact: interval_open] => + _ .
+  + by apply: open_comp; [|exact: interval_open].
+  + by apply: open_comp; [|exact: interval_open].
   + by apply: fa0; rewrite set_itvoo => x /= ->; apply/andP; split.
   + apply: fb1; rewrite set_itvoo => x /= ->. 
     by rewrite ltr_pdivr_mulr // mul1r Bool.andb_diag ltr_addl. 
@@ -4212,15 +4214,15 @@ move=> + A clA B /set_nbhsP [C [oC AC CB]].
 have AC0 : A `&` ~` C = set0 by apply/disjoints_subset; rewrite setCK.
 case/(_ _ _ clA (open_closedC oC) AC0)=> U [V] [oU oV AU nCV UV0].
 exists (~` (closure V)).
-  apply/set_nbhsP; exists (U); split => //. 
-  apply/subsetCr; have := (open_closedC oU); rewrite closure_id => ->. 
+  apply/set_nbhsP; exists (U); split => //.
+  apply/subsetCr; have := (open_closedC oU); rewrite closure_id => ->.
   by apply: closure_subset; apply/disjoints_subset; rewrite setIC.
 apply: (subset_trans _ CB); apply/subsetCP; apply: (subset_trans nCV).
-apply/subsetCr; have := (open_closedC oV); rewrite closure_id => ->. 
+apply/subsetCr; have := (open_closedC oV); rewrite closure_id => ->.
 by apply: closure_subset; apply/subsetC; exact: subset_closure.
 Qed.
 
-Lemma normal_openP : normal_space T <-> 
+Lemma normal_openP : normal_space T <->
   forall (A B : set T), closed A -> closed B -> A `&` B = set0 ->
   exists U V, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0].
 Proof. exact: (normal_spaceP 0%N 2%N). Qed.
@@ -4232,21 +4234,22 @@ Proof. exact: (normal_spaceP 0%N 1%N). Qed.
 End normalP.
 
 Section pseudometric_normal.
+
 Lemma uniform_regular {X : uniformType} : @regular_space X.
 Proof.
 move=> x A; rewrite /= -nbhs_entourageE; case => E entE.
 move/(subset_trans (ent_closure entE)) => ?.
 by exists [set y | (split_ent E) (x, y)]; first by exists (split_ent E).
 Qed.
 
-Lemma regular_openP {T : topologicalType} (x : T) : 
-  {for x, @regular_space T} <-> (forall A, closed A -> ~ A x -> exists (U V : set T),
-    [/\ open U, open V, U x, A `<=` V & U `&` V = set0]).
+Lemma regular_openP {T : topologicalType} (x : T) :
+  {for x, @regular_space T} <-> (forall A, closed A -> ~ A x ->
+  exists (U V : set T), [/\ open U, open V, U x, A `<=` V & U `&` V = set0]).
 Proof.
 split.
   move=> + A clA nAx => /(_ (~` A)) [].
     by apply: open_nbhs_nbhs; split => //; apply: closed_openC.
-  move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U). 
+  move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U).
   exists (~` (closure U)); split => //; first exact: open_interior.
     by apply: closed_openC; exact: closed_closure.
   apply/disjoints_subset; rewrite setCK; apply: (@subset_trans _ U).
@@ -4257,11 +4260,11 @@ move=> + A Ax => /(_ (~` (interior A))) []; [|exact|].
 move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U.
   by apply: open_nbhs_nbhs; split.
 apply: subset_trans; first exact: (closure_subset UV).
-move/open_closedC/closure_id:oV => <-.
+move/open_closedC/closure_id: oV => <-.
 apply: (subset_trans cAV); rewrite setCK; exact: interior_subset.
 Qed.
 
-Lemma pseudometric_normal {R : realType} {X : pseudoMetricType R} : 
+Lemma pseudometric_normal {R : realType} {X : pseudoMetricType R} :
   normal_space X.
 Proof.
 apply/(@normal_openP _ R) => A B clA clB AB0.
@@ -4290,8 +4293,8 @@ case: (pselect ((epsA x)%:num/2 <= (epsB y)%:num/2)).
   move/ball_sym:Axe =>/[swap] /le_ball /[apply] /(ball_triangle Bye). 
   rewrite -splitr => byx; have := projT2 (cid (eps' _ clA y)) nAy.
   by rewrite -subset0; apply; split; first exact: byx.
-move/negP; rewrite leNgt negbK => /ltW. 
-move/ball_sym:Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe). 
+move/negP; rewrite leNgt negbK => /ltW.
+move/ball_sym:Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe).
 rewrite -splitr => byx; have := projT2 (cid (eps' _ clB x)) nBx.
 by rewrite -subset0; apply; split; first exact: byx.
 Qed.