Scope the notation for value, restrict, range

Author: Convindix

Foundation/FirstOrder/SetTheory/Function.lean

@@ -383,7 +383,7 @@ noncomputable def value (f x : V) : V := {z ∈ ⋃ˢ range f ; ∃ y, z ∈ y 
 -- noncomputable def value {X Y : V} (f x : V) (hf : f ∈ Y ^ X) (hx : x ∈ X) : V := Classical.choose! ((mem_function_iff.mp hf).2 x hx)
 
 /-- If `x` is in `domain f`, then `f ‘ x` is the value of `f` at `x`, else it is `∅`.-/
-notation f:arg " ‘ " x:arg => value f x
+scoped notation f:arg " ‘ " x:arg => value f x
 
 def value.dfn : Semisentence ℒₛₑₜ 3 := f“v f x. ∀ z, z ∈ v ↔ z ∈ !sUnion.dfn (!range.dfn f) ∧ ∃ y, z ∈ y ∧ !kpair.dfn x y ∈ f”
 
@@ -409,7 +409,7 @@ lemma value_mem_range (f x : V) {X Y : V} {hf : f ∈ Y ^ X} {hx : x ∈ X} : f
 noncomputable def restrict (R A : V) : V := R ∩ (A ×ˢ range R)
 
 /-- Restricting the domain of a relation -/
-notation R:arg " ↾ " A:arg => restrict R A
+scoped notation R:arg " ↾ " A:arg => restrict R A
 
 def restrict.dfn : Semisentence ℒₛₑₜ 3 := f“r R A. r = !inter.dfn R (!prod.dfn A (!range.dfn R))”
 
@@ -433,7 +433,7 @@ lemma domain_restrict_eq (R A : V) : domain (R ↾ A) = domain R ∩ A := by
 noncomputable def image (R A : V) : V := range (restrict R A)
 
 /-- Image of a set under a relation -/
-notation R:arg " “ " A:arg => restrict R A
+scoped notation R:arg " “ " A:arg => restrict R A
 
 def image.dfn : Semisentence ℒₛₑₜ 3 := f“B R A. B = !range.dfn (!restrict.dfn R A)”