Unscoped `⋃₀` and `⋂₀`

Stream: mathlib4

[Yakov Pechersky]

We have unscoped notation in ZFC files:

import Mathlib

/-
Ambiguous term
  ⋂₀ _
Possible interpretations:
  ⋂₀ ?m.2 : Class.{?u.1}

  ⋂₀ ?m.5 : ZFSet.{?u.4}

  ⋂₀ ?m.8 : Set ?m.7
-/
#check ⋂₀ _

Should we scope these? src#Class.sUnion

/-- The union of a class is the class of all members of ZFC sets in the class -/
def sUnion (x : Class) : Class :=
  ⋃₀ classToCong x

@[inherit_doc]
prefix:110 "⋃₀ " => Class.sUnion

/-- The intersection of a class is the class of all members of ZFC sets in the class -/
def sInter (x : Class) : Class :=
  ⋂₀ classToCong x

@[inherit_doc]
prefix:110 "⋂₀ " => Class.sInter

[Miyahara Kō]

Yakov Pechersky said:

We have unscoped notation in ZFC files:

import Mathlib

/-
Ambiguous term
  ⋂₀ _
Possible interpretations:
  ⋂₀ ?m.2 : Class.{?u.1}

  ⋂₀ ?m.5 : ZFSet.{?u.4}

  ⋂₀ ?m.8 : Set ?m.7
-/
#check ⋂₀ _

Should we scope these? src#Class.sUnion

/-- The union of a class is the class of all members of ZFC sets in the class -/
def sUnion (x : Class) : Class :=
  ⋃₀ classToCong x

@[inherit_doc]
prefix:110 "⋃₀ " => Class.sUnion

/-- The intersection of a class is the class of all members of ZFC sets in the class -/
def sInter (x : Class) : Class :=
  ⋂₀ classToCong x

@[inherit_doc]
prefix:110 "⋂₀ " => Class.sInter

Personally, I think instead of scoping them, it would be better to turn them into a notation class, like in docs#Union.

[Yakov Pechersky]

#27833