# Zulip Chat Archive

## Stream: new members

### Topic: Ultra-noob set question

#### Chris Staecker (Aug 12 2021 at 17:26):

Ultra-noob here, sorry if this is a stupid question: I am stumped trying to make simple definitions of sets. I want to define $N_0$ as the set of even natural numbers, $N_1$ as the odds. Then $C_0 = \{0\} \times \{0,1\} \times N_0$ and $C_1 = \{1\} \times \{0,1\} \times N_1$. And THEN $C = C_0 \cup C_1 \cup (\{-1\}\times \{-1\} \times \{0,1\})$.

Here is my attempt:

```
import data.set
import data.nat.basic
open set
def N_0 : set ℕ := { n:ℕ | even n }
def N_1 : set ℕ := { n:ℕ | odd n }
def C_0 := ({0}:set ℤ) × ({0,1}:set ℤ) × N_0
def C_1 := ({1}:set ℤ) × ({0,1}:set ℤ) × N_1
def C := C_0 ∪ C_1 ∪ ({(-1, -1,0)}:set (ℤ × ℤ × ℕ))
```

Most of this works, though I'm not sure I'm doing the best way (are my type annotations appropriate?). But the last line is complaining, I think it doesn't know how to build the unions. But I'm not sure how to tell it.

Thanks for any help-

#### Eric Wieser (Aug 12 2021 at 17:53):

Some Zulip formatting tips: `$$ $$`

for latex, #backticks for code - could you edit your post to adjust that?

#### Eric Wieser (Aug 12 2021 at 17:55):

What exactly do you intent to be the meaning of `×`

? Because as you have it, `N_0`

is a `set nat`

but `C_0`

is a `Type`

. Did you intend `C_0`

to have type`set (ℤ × ℕ × ℕ)`

?

#### Eric Wieser (Aug 12 2021 at 17:57):

If so, you need docs#set.prod instead of `×`

(docs#prod)

#### Chris Staecker (Aug 12 2021 at 18:12):

Thanks very much! You are right I want × to be a cartesian product of sets. I'll try set.prod. Can I somehow cause the × symbol to give me set.prod instead of prod?

#### Eric Wieser (Aug 12 2021 at 21:15):

Well you're using it as `prod`

in other parts of your expression, so that wouldn't work so well

#### Eric Wieser (Aug 12 2021 at 21:16):

Note that you can at least use `s.prod t`

for the Cartesian product of s and t - you don't have to write `set.prod s t`

#### Chris Staecker (Aug 12 2021 at 21:39):

I have had good luck changing all of my products to set.prod. Was that a bad idea? I intended for all those def's to define specific sets.

Also- is it possible to make cartesian triples? I made my own infix name for set.prod, and using this to build a triple results in a pair-of-pairs like ((x,y),z). Is that the best I can do? Or can I make it give me (x,y,z)? Thanks-

#### Mario Carneiro (Aug 12 2021 at 21:40):

you can write `s1.prod $ s2.prod s3`

to get the right associated product of sets

#### Mario Carneiro (Aug 12 2021 at 21:41):

(note, `(x,y,z)`

is right associated, i.e. `(x,(y,z))`

in lean)

#### Chris Staecker (Aug 12 2021 at 21:41):

awesome- thanks!

#### Mario Carneiro (Aug 12 2021 at 21:41):

same for `ℤ × ℕ × ℕ := ℤ × (ℕ × ℕ)`

Last updated: Dec 20 2023 at 11:08 UTC