## 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 typeset (ℤ × ℕ × ℕ)?

#### 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)

awesome- thanks!

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

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

Last updated: Dec 20 2023 at 11:08 UTC