Building sets

Stream: new members

[Emiel Lanckriet]

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]

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

[Bryan Gin-ge Chen]

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

[Chris Hughes]

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

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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

[Emiel Lanckriet]

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]

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

[Bryan Gin-ge Chen]

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]

Remember this notation is randomly broken

[Patrick Massot]

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

[Kenny Lau]

wrong link?

[Patrick Massot]

Fixed

[Patrick Massot]

Thanks Kenny

[Kenny Lau]

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]

But how do I arrive at a Prop?

[Kenny Lau]

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

[Kenny Lau]

a Prop is just a true/false statement

[Emiel Lanckriet]

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