From bc2966309352d746251f4efb1af9e5f73438cecf Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 29 Nov 2023 06:08:23 +0000 Subject: [PATCH] fix: Use notation3 for neighborhood notations (#8690) The point is to get delaborators for free. This was previously blocked on `notation3` not supporting `scoped`. --- Mathlib/Topology/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index d2b36293f56bc..96355bb3caabc 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -848,19 +848,19 @@ scoped[Topology] notation "๐“" => nhds scoped[Topology] notation "๐“[" s "] " x:100 => nhdsWithin x s /-- Notation for the filter of punctured neighborhoods of a point. -/ -scoped[Topology] notation "๐“[โ‰ ] " x:100 => nhdsWithin x (@singleton _ (Set _) instSingletonSet x)แถœ +scoped[Topology] notation3 "๐“[โ‰ ] " x:100 => nhdsWithin x (@singleton _ (Set _) instSingletonSet x)แถœ /-- Notation for the filter of right neighborhoods of a point. -/ -scoped[Topology] notation "๐“[โ‰ฅ] " x:100 => nhdsWithin x (Set.Ici x) +scoped[Topology] notation3 "๐“[โ‰ฅ] " x:100 => nhdsWithin x (Set.Ici x) /-- Notation for the filter of left neighborhoods of a point. -/ -scoped[Topology] notation "๐“[โ‰ค] " x:100 => nhdsWithin x (Set.Iic x) +scoped[Topology] notation3 "๐“[โ‰ค] " x:100 => nhdsWithin x (Set.Iic x) /-- Notation for the filter of punctured right neighborhoods of a point. -/ -scoped[Topology] notation "๐“[>] " x:100 => nhdsWithin x (Set.Ioi x) +scoped[Topology] notation3 "๐“[>] " x:100 => nhdsWithin x (Set.Ioi x) /-- Notation for the filter of punctured left neighborhoods of a point. -/ -scoped[Topology] notation "๐“[<] " x:100 => nhdsWithin x (Set.Iio x) +scoped[Topology] notation3 "๐“[<] " x:100 => nhdsWithin x (Set.Iio x) end