Zulip Chat Archive

Stream: new members

Topic: ordered pairs


view this post on Zulip 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)?

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:54):

what do you mean by "right notation"?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:54):

A notation that works in Lean.

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:54):

do you mean set (X × Y)?

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:54):

oh

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:55):

No, I mean for the ordered pairs.

view this post on Zulip 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 }

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:57):

Ah.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 22:57):

Thanks.

view this post on Zulip 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}

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:58):

you can't define that in ZFC either

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:58):

you need to use specification and an existential

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 22:59):

I guess you could use set.image or set.range, whatever it's called

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:02):

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

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:03):

(after import data.set.basic)

view this post on Zulip 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)}

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:07):

What's ?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 18 2018 at 23:08):

set X is a complete lattice

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:08):

Abhi: is notation so you can start with #print notation ⨆

view this post on Zulip 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 :-)

view this post on Zulip 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 :-/

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:11):

eq.symm only goes one way

view this post on Zulip Kenny Lau (Oct 18 2018 at 23:11):

eq_comm

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:12):

oh oops

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:12):

yes that is impossible to interpret

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:13):

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

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:13):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:14):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:14):

I get "no definition found"

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:14):

It's the analogue of \bigcup for lattices

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:14):

It's in order/complete_lattice.lean

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:14):

notation binders , r:(scoped f, supr f) := r

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:15):

I taught Abhi about bigcup today in lectures :-)

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:16):

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

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:17):

"day to day life"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:18):

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

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:19):

so supr s is the supremum of the range of s

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:23):

I can't make sense of that definition

view this post on Zulip Reid Barton (Oct 18 2018 at 23:23):

I would make f an explicit argument and then pass it in p1

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:24):

what does g : graph mean?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:24):

it's not a type

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:26):

Keep in mind that graph fis not a type either, it's a set

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:27):

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

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 18 2018 at 23:28):

so you should start with ext X Y f

view this post on Zulip 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}

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:29):

I am in the middle of showing my graph is Kenny's supr thing

view this post on Zulip Kenny Lau (Oct 18 2018 at 23:30):

I bet example : graph = graph' := isn't what Kevin wanted us to prove

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:30):

I proved that using eq.comm

view this post on Zulip Kenny Lau (Oct 18 2018 at 23:30):

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

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 23:34):

I am not proud of the second one though.

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:37):

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

view this post on Zulip 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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:38):

Is the notation for ordered pairs different for subtypes?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 23:38):

so the X value is g.1.1

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:39):

That works, but I don't get why.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:39):

(deleted)

view this post on Zulip Reid Barton (Oct 18 2018 at 23:39):

or g.val.fst

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 18 2018 at 23:46):

Why does the same convention not apply to sets?

view this post on Zulip 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