Zulip Chat Archive

Stream: new members

Topic: Building sets


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Apr 25 2020 at 09:26):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 25 2020 at 09:28):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 25 2020 at 09:29):

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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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 )}

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:39):

Remember this notation is randomly broken

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:40):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 09:40):

wrong link?

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:43):

Fixed

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:43):

Thanks Kenny

view this post on Zulip 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

view this post on Zulip Emiel Lanckriet (Apr 25 2020 at 09:45):

But how do I arrive at a Prop?

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 25 2020 at 09:47):

a Prop is just a true/false statement

view this post on Zulip 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