# Zulip Chat Archive

## Stream: new members

### Topic: ordered pairs

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:53):

I'm defining a subset of the Cartesian product of two types, specifically:

def graph : set X × Y := {(x : X, f x) | x : X}

(`f`

is a function, `x`

has not been separately defined) What's the right notation for this (the ordered pairs, and also the set builder itself)?

#### Kenny Lau (Oct 18 2018 at 22:54):

what do you mean by "right notation"?

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:54):

A notation that works in Lean.

#### Kenny Lau (Oct 18 2018 at 22:54):

do you mean `set (X × Y)`

?

#### Kenny Lau (Oct 18 2018 at 22:54):

oh

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:55):

No, I mean for the ordered pairs.

#### Kenny Lau (Oct 18 2018 at 22:56):

universes u v variables {X : Type u} {Y : Type v} (f : X → Y) def graph : set (X × Y) := { z | z.2 = f z.1 }

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:57):

Ah.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:57):

Thanks.

#### Kevin Buzzard (Oct 18 2018 at 22:58):

It's kind of annoying that you can't write `{⟨x,y⟩ : X × Y | y = f x}`

#### Kenny Lau (Oct 18 2018 at 22:58):

you can't define that in ZFC either

#### Kenny Lau (Oct 18 2018 at 22:58):

you need to use specification and an existential

#### Kevin Buzzard (Oct 18 2018 at 22:59):

I guess you could use `set.image`

or `set.range`

, whatever it's called

#### Kevin Buzzard (Oct 18 2018 at 23:02):

`def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩) `

#### Kevin Buzzard (Oct 18 2018 at 23:03):

(after `import data.set.basic`

)

#### Kenny Lau (Oct 18 2018 at 23:04):

import data.set.lattice universes u v variables {X : Type u} {Y : Type v} (f : X → Y) def graph : set (X × Y) := ⨆ x : X, {(x, f x)}

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:07):

What's `⨆`

?

#### Kevin Buzzard (Oct 18 2018 at 23:08):

import data.set.basic variables (X Y : Type) (f : X → Y) def graph : set (X × Y) := {z : X × Y | z.2 = f z.1} def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩) example : graph = graph' := sorry

#### Kenny Lau (Oct 18 2018 at 23:08):

`set X`

is a complete lattice

#### Kevin Buzzard (Oct 18 2018 at 23:08):

Abhi: `⨆`

is notation so you can start with `#print notation ⨆`

#### Kevin Buzzard (Oct 18 2018 at 23:09):

but if you don't want to go down the lattice rabbithole you could try my homework :-)

#### Kevin Buzzard (Oct 18 2018 at 23:11):

I'd be able to do the homework myself if I knew how to prove `A = B iff B = A`

:-/

#### Kevin Buzzard (Oct 18 2018 at 23:11):

`eq.symm`

only goes one way

#### Kenny Lau (Oct 18 2018 at 23:11):

eq_comm

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:11):

I'm not sure how to interpret the results of #print notation. All I get is `'⨆':1024 binders ',':0 (scoped 0) := #0`

What's a binder?

#### Kevin Buzzard (Oct 18 2018 at 23:12):

oh oops

#### Kevin Buzzard (Oct 18 2018 at 23:12):

yes that is impossible to interpret

#### Kevin Buzzard (Oct 18 2018 at 23:13):

A binder is something like forall or exists or lambda I think

#### Kevin Buzzard (Oct 18 2018 at 23:13):

Kenny is using `⨆`

in the same sort of way that one would use those things.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:14):

Yeah, I can tell it's something like forall, but I'm not sure what the difference is.

#### Mario Carneiro (Oct 18 2018 at 23:14):

I think you can click on the sup to go to definition

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:14):

I get "no definition found"

#### Mario Carneiro (Oct 18 2018 at 23:14):

It's the analogue of `\bigcup`

for lattices

#### Kevin Buzzard (Oct 18 2018 at 23:14):

It's in `order/complete_lattice.lean`

#### Kevin Buzzard (Oct 18 2018 at 23:14):

`notation `

⨆` binders `

, ` r:(scoped f, supr f) := r`

#### Kevin Buzzard (Oct 18 2018 at 23:15):

I taught Abhi about bigcup today in lectures :-)

#### Kevin Buzzard (Oct 18 2018 at 23:16):

Glad to see my lectures are coming in handy in his day to day life

#### Mario Carneiro (Oct 18 2018 at 23:17):

"day to day life"

#### Kevin Buzzard (Oct 18 2018 at 23:17):

I don't understand that notation line at all. I think notation in Lean is somehow evil; most of it is fine and then there are some weird hacks which I don't get at all. The key point is `supr`

somehow, and then everything else is some notation mantra I guess

#### Kevin Buzzard (Oct 18 2018 at 23:18):

`def supr [complete_lattice α] (s : ι → α) : α := Sup {a : α | ∃i : ι, a = s i}`

#### Kevin Buzzard (Oct 18 2018 at 23:19):

so `supr s`

is the supremum of the range of `s`

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:22):

Btw I'm trying `def p1 (g : graph) : X := g.1`

based on the earlier definition of `graph`

, but it doesn't work:

invalid field notation, type is not of the form (C ...) where C is a constant g has type ⁇

universe u variable {X : Type u} variable {Y : Type u} variable {f : X → Y} def graph : set (X × Y) := { g | g.2 = f g.1 } def p1 (g : graph) : X := g.1

I guess part of the problem is that `G`

is not a type -- I tried coercing it as `↑G`

, but that just produces more errors.

#### Reid Barton (Oct 18 2018 at 23:23):

I think the bigger problem is Lean doesn't know what you want to take the graph of

#### Mario Carneiro (Oct 18 2018 at 23:23):

I can't make sense of that definition

#### Reid Barton (Oct 18 2018 at 23:23):

I would make `f`

an explicit argument and then pass it in `p1`

#### Mario Carneiro (Oct 18 2018 at 23:24):

what does `g : graph`

mean?

#### Mario Carneiro (Oct 18 2018 at 23:24):

it's not a type

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:25):

what does

`g : graph`

mean?

Yeah, I realise that, but I want to show (separately from the definition) it's a bijection from `graph`

to `X`

.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:26):

I would make

`f`

an explicit argument and then pass it in`p1`

Indeed that removes the first error. How, though?

#### Mario Carneiro (Oct 18 2018 at 23:26):

Keep in mind that `graph f`

is not a type either, it's a set

#### Mario Carneiro (Oct 18 2018 at 23:27):

lean knows to coerce from a set to a type, but maybe you want the subtype instead?

#### Kevin Buzzard (Oct 18 2018 at 23:27):

a set is a term not a Type Abhi. Did you come to my lecture today?

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:28):

a set is a term not a Type Abhi. Did you come to my lecture today?

I realise that -- but how else would I later show it to be a bijection from graph to X?

#### Kevin Buzzard (Oct 18 2018 at 23:28):

If `X`

is a type and `p : X -> Prop`

then in Lean there are two very different ways to express what in set theory is just "the subset of X consisting of elements `a`

for which `p a`

is true"

#### Kenny Lau (Oct 18 2018 at 23:28):

it did took me some time to figure out that Kevin wants us to prove that the two big big functions `graph`

and `graph'`

are equal

#### Kenny Lau (Oct 18 2018 at 23:28):

so you should start with `ext X Y f`

#### Kevin Buzzard (Oct 18 2018 at 23:28):

One is the set `{x : X | p x}`

and one is the subtype `{x : X // p x}`

#### Kevin Buzzard (Oct 18 2018 at 23:29):

I am in the middle of showing my `graph`

is Kenny's `supr`

thing

#### Kenny Lau (Oct 18 2018 at 23:30):

I bet `example : graph = graph' :=`

isn't what Kevin wanted us to prove

#### Kevin Buzzard (Oct 18 2018 at 23:30):

I proved that using `eq.comm`

#### Kenny Lau (Oct 18 2018 at 23:30):

`example : graph X Y f = graph' X Y f :=`

#### Kevin Buzzard (Oct 18 2018 at 23:34):

import data.set.basic import data.set.lattice variables (X Y : Type) (f : X → Y) def graph : set (X × Y) := {z : X × Y | z.2 = f z.1} def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩) def graph'' : set (X × Y) := ⨆ x : X, {(x, f x)} example : graph = graph' := sorry example : graph = graph'' := sorry

I did them both :-)

#### Kevin Buzzard (Oct 18 2018 at 23:34):

I am not proud of the second one though.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:36):

Re:the bijection, I *can* write `def p1 (g : graph f) := g.1`

(still defining `graph`

as a set because subtype gives me even more errors), but then `p1`

for some reason has the wrong type. Apparently `g.1`

isn't processed correctly (it still has type `X × Y`

and not `X`

).

#### Mario Carneiro (Oct 18 2018 at 23:37):

that has to do with the fact that it is a subtype

#### Mario Carneiro (Oct 18 2018 at 23:38):

`g`

is a pair of an element of `X x Y`

and a proof that this element satisfies `z.2 = f z.1`

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:38):

Is the notation for ordered pairs different for subtypes?

#### Mario Carneiro (Oct 18 2018 at 23:38):

so the X value is `g.1.1`

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:39):

That works, but I don't get why.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:39):

(deleted)

#### Reid Barton (Oct 18 2018 at 23:39):

or `g.val.fst`

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:40):

Ok, I get the argument, but I'm not sure why it's defined that way (to include a proof).

#### Reid Barton (Oct 18 2018 at 23:43):

If you didn't have to provide a proof when constructing a value of the subtype, then it would just be the same as the entire original type.

#### Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:46):

Why does the same convention not apply to sets?

#### Reid Barton (Oct 18 2018 at 23:49):

I don't really understand the question. A set is not a type; perhaps that's the answer

Last updated: May 11 2021 at 13:22 UTC