fixes #1042

math-comp · Oct 11, 2023 · caabd47 · caabd47
1 parent 7f238c0
commit caabd47
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,9 @@
 
 ### Generalized
 
+- in `topology.v`:
+  + `ball_filter` generalized to `realDomainType`
+
 ### Deprecated
 
 ### Removed

diff --git a/theories/topology.v b/theories/topology.v
@@ -5479,17 +5479,20 @@ move=> e_gt0 PP y; rewrite in_itv/= -ler_distlC => ye; apply: PP => /=.
 by rewrite (le_lt_trans ye)// ltr_pMl// ltr1n.
 Qed.
 
-Global Instance ball_filter (R : realFieldType) (t : R) : Filter
+Global Instance ball_filter (R : realDomainType) (t : R) : Filter
   [set P | exists2 i : R, 0 < i & ball_ Num.norm t i `<=` P].
 Proof.
 apply: Build_Filter; [by exists 1 | move=> P Q | move=> P Q PQ]; rewrite /mkset.
 - move=> -[x x0 xP] [y ? yQ]; exists (Num.min x y); first by rewrite lt_minr x0.
   move=> z tz; split.
-  by apply: xP; rewrite /= (lt_le_trans tz) // le_minl lexx.
+    by apply: xP; rewrite /= (lt_le_trans tz) // le_minl lexx.
   by apply: yQ; rewrite /= (lt_le_trans tz) // le_minl lexx orbT.
 - by move=> -[x ? xP]; exists x => //; apply: (subset_trans xP).
 Qed.
 
+#[global] Hint Extern 0 (Filter [set P | exists2 i, _ & ball_ _ _ i `<=` P]) =>
+  (apply: ball_filter) : typeclass_instances.
+
 Section pseudoMetric_of_normedDomain.
 Context {K : numDomainType} {R : normedZmodType K}.
 Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.norm x e x.