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

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 }


Ah.

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

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?

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?

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 fis 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.

(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