## Stream: new members

### Topic: Building sets

#### Emiel Lanckriet (Apr 25 2020 at 09:15):

I want to build a set that contains {(0,0), (1, 1), (1, 0), (0,1)} without just summing them, but I can't seem to find how,
I tried:

set.prod {0, 1} {0, 1}


and

{(x, y) | ∀ x y : ℤ, x y ∈ {0, 1}}


But in the first instance CoCalc doesn't recognise set.prod, this might be an import problem, but in the Mathlib I can't find what I should import specifically.
For the second attempt the compiler just says that it use sorry, even though I don't.
Could anyone tell what went wrong in these two examples?

#### Chris Hughes (Apr 25 2020 at 09:26):

import data.set.basic will probably make the first one work.

#### Bryan Gin-ge Chen (Apr 25 2020 at 09:27):

For the second, you could use {p : ℤ × ℤ | p.1 ∈ {0,1} ∧ p.2 ∈ {0,1}} instead.

#### Chris Hughes (Apr 25 2020 at 09:27):

The second notation isn't supported by Lean, there has to be a single variable to the left of the vertical bar.

#### Kenny Lau (Apr 25 2020 at 09:28):

why do you want to build {(0,0),(1,1),(1,0),(0,1)}?

#### Bryan Gin-ge Chen (Apr 25 2020 at 09:29):

Maybe this notation could be made to work in Lean 4.

#### Emiel Lanckriet (Apr 25 2020 at 09:33):

If I try {p : ℤ × ℤ | p.1 ∈ {0,1} ∧ p.2 ∈ {0,1}} as Bryan suggested then I get the error:

don't know how to synthesize placeholder
context:
p : ℤ × ℤ
⊢ Type ?


#### Emiel Lanckriet (Apr 25 2020 at 09:34):

I want to build this set for the exercise on Codewars about symmetric and transitive relations that are not reflexive.

#### Bryan Gin-ge Chen (Apr 25 2020 at 09:38):

Oh, that's weird. It worked in #check.

Making an edit because this no longer matters. This works:

def foo : set (ℤ × ℤ) := {p : ℤ × ℤ | p.1 ∈ ({0,1} : set ℤ) ∧ p.2 ∈ ({0,1} : set ℤ)}


#### Patrick Massot (Apr 25 2020 at 09:39):

Remember this notation is randomly broken

#### Patrick Massot (Apr 25 2020 at 09:40):

And here you mix it with another notoriously broken notation {0, 1}

Fixed

Thanks Kenny

#### Kenny Lau (Apr 25 2020 at 09:44):

Emiel Lanckriet said:

I want to build this set for the exercise on Codewars about symmetric and transitive relations that are not reflexive.

if you want to build a relation, you can just build a proposition Z -> Z -> Prop without going through the set-theoretic nonsense

#### Emiel Lanckriet (Apr 25 2020 at 09:45):

But how do I arrive at a Prop?

#### Kenny Lau (Apr 25 2020 at 09:47):

for example, the above set would be λ p q, (p = 0 ∨ p = 1) ∧ (q = 0 ∨ q = 1)

#### Kenny Lau (Apr 25 2020 at 09:47):

a Prop is just a true/false statement

#### Emiel Lanckriet (Apr 25 2020 at 09:48):

Ah, ok, thanks, that should indeed make my live easier.

Last updated: May 08 2021 at 04:14 UTC