Ultra-noob set question

Stream: new members

[Chris Staecker]

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]

Some Zulip formatting tips: $$ $$ for latex, #backticks for code - could you edit your post to adjust that?

[Eric Wieser]

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]

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

[Chris Staecker]

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]

Well you're using it as prod in other parts of your expression, so that wouldn't work so well

[Eric Wieser]

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]

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]

you can write s1.prod $ s2.prod s3 to get the right associated product of sets

[Mario Carneiro]

(note, (x,y,z) is right associated, i.e. (x,(y,z)) in lean)

[Chris Staecker]

awesome- thanks!

[Mario Carneiro]

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