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 N0N_0 as the set of even natural numbers, N1N_1 as the odds. Then C0={0}×{0,1}×N0C_0 = \{0\} \times \{0,1\} \times N_0 and C1={1}×{0,1}×N1C_1 = \{1\} \times \{0,1\} \times N_1. And THEN C=C0C1({1}×{1}×{0,1})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)

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