Zulip Chat Archive

Stream: new members

Topic: sum of sets

Patrick Thomas (Jul 23 2020 at 01:15):

I am trying to understand why this fails and how to fix it:

import data.real.basic

def set_sum : set ℝ → set ℝ → set ℝ
| (X : set ℝ) (Y : set ℝ) := {x + y | x ∈ X ∧ y ∈ Y}

Alex J. Best (Jul 23 2020 at 01:21):

It fails because lean's set notation doesn't support this, specifically the thing left of the | must just be an identifier like x.
This definition already exists in algebra/pointwise.lean

Alex J. Best (Jul 23 2020 at 01:22):

The definition there is as:

instance [has_add α] : has_add (set α) := ⟨image2 has_add.add⟩

Alex J. Best (Jul 23 2020 at 01:22):

And image2 is

def image2 (f : α → β → γ) (s : set α) (t : set β) : set γ :=
{c | ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c }

Alex J. Best (Jul 23 2020 at 01:23):

There were some interesting related threads to do with changing this notation earlier today btw, https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23402.3A.20set.20builder.20notation/near/204661344

Patrick Thomas (Jul 23 2020 at 01:27):

Thank you.

Patrick Thomas (Jul 23 2020 at 01:32):

So I need to do this?

def set_sum : set ℝ → set ℝ → set ℝ
| (X : set ℝ) (Y : set ℝ) := {z | ∃ x ∈ X, ∃ y ∈ Y, z = x + y}

Alex J. Best (Jul 23 2020 at 01:35):

Yeah that looks like it should work, does it?

Patrick Thomas (Jul 23 2020 at 01:36):

Yeah.

Patrick Thomas (Jul 23 2020 at 01:38):

Does the existing definition allow for writing something like X + Y?

Patrick Thomas (Jul 23 2020 at 01:39):

I tried that, but no luck. Not sure if I have it right though.

Patrick Thomas (Jul 23 2020 at 01:39):

For example:
def set_sum : set ℝ → set ℝ → set ℝ
| (X : set ℝ) (Y : set ℝ) := X + Y

Patrick Thomas (Jul 23 2020 at 01:40):

Not sure how to read the definition exactly.

Alex J. Best (Jul 23 2020 at 01:40):

Yes, because it is registered as a has_add instance. It works for me, are you importing algebra.pointwise

Reid Barton (Jul 23 2020 at 01:40):

Do you have it imported?

Patrick Thomas (Jul 23 2020 at 01:40):

Ah. Right. Sorry.

Patrick Thomas (Jul 23 2020 at 01:42):

Hmm. No, this does not work for me.

import data.real.basic
import data.set
import algebra.pointwise

def set_sum : set ℝ → set ℝ → set ℝ
| (X : set ℝ) (Y : set ℝ) := X + Y

Patrick Thomas (Jul 23 2020 at 01:44):

I get:

failed to synthesize type class instance for
set_sum : set ℝ → set ℝ → set ℝ,
X Y : set ℝ
⊢ has_add (set ℝ)

Bryan Gin-ge Chen (Jul 23 2020 at 01:53):

What version of mathlib are you using? Try leanproject up to get a more recent version.

Bryan Gin-ge Chen (Jul 23 2020 at 01:53):

Also note that you can get nice syntax highlighting on Zulip using #backticks.

Patrick Thomas (Jul 23 2020 at 01:56):

I'm not sure I have the command leanproject.

Bryan Gin-ge Chen (Jul 23 2020 at 01:59):

The community Lean tooling has been revamped in the past few months: try going through the #install instructions for your OS again. There's even tutorial videos!

Patrick Thomas (Jul 23 2020 at 02:01):

It has been a while since I used it. I'll give it a try. Thank you.

Last updated: Feb 28 2026 at 14:05 UTC