mathlib import needed to support pointwise set ops

Stream: new members

[Rado Kirov]

I want set +, * ops to work pointwise on set of reals, but according to AIs i need to import the right mathlib file. However, but they keep hallucinating the file needed, so I need to ask the friendly humans here instead.

import Mathlib
import Mathlib.Data.Set.Basic -- not the right import

def x : Set Real := {0, 1}
def y : Set Real := {0, 2}
def z := x + y -- should be {0 + 0, 1 + 0, 0 + 2, 1 + 2} but doesn't work

def f := fun (n:ℕ) ↦ n + 1
def g := fun (n:ℕ) ↦ n + 2
def h := f + g  -- works just fine without imports

A bit annoying that for functions this just works out of the box, but for sets I need imports.

[Lawrence Wu (llllvvuu)]

docs#Set.add and you need to open scoped Pointwise

[Rado Kirov]

Thank you!