## Stream: new members

### Topic: Help with explicit sets

#### Robert Spencer (Apr 08 2019 at 16:42):

I've been battling a while now with sets, finsets, fintypes and such forth for a while now. I have many questions, but as way of a first one I have this.

Given the following definition of a quiver:

variables {α β : Type}

structure quiver :=
(vertices : set α)
(edges : set β)
(s : edges → vertices)
(t : edges → vertices)


I would like to define a small "toy" example so I can prove some theorems with it. Something like

variables (A B : α ) (a : β )  [decidable_eq α] [decidable_eq β]

def test_quiver : @quiver α β :=
{
vertices := {A, B},
edges := {a},
s := λ e, A,
t := λ e, B,
}


A lot about this screams sub-optimal to me: for example the s and t functions I'd prefer to define by some mapping from a to values (so that defining more complicated quivers is simple). I presume there is some way to do this with inductive functions, but that is secondary.

The first problem is that the above doesn't compile.

/home/rob...ry/src/quiver.lean:40:9: error: type mismatch at field 's'
λ (e : ↥{a}), A
has type
↥{a} → α
but is expected to have type
↥{a} → ↥{A, B}


I understand the error, and I understand the problem (A is of type α and a priori has nothing to do with the set {A, B}). My question is how to fix this? Since I can't even find where the {...} notation is defined, I don't know what type {A,B} even is, so don't know what is missing.

#### Reid Barton (Apr 08 2019 at 16:45):

You've defined "a quiver whose vertices are a subset of α and whose edges are a subset of β". Unless you really meant to do this for some reason, it would probably make things a lot easier to define

structure quiver :=
(vertices : Type)
(edges : Type)
(s : edges → vertices)
(t : edges → vertices)


#### Robert Spencer (Apr 08 2019 at 16:50):

Ok, sure: I suppose that makes a little more sense (and coercion will convert any subsets of type α to a type when I need to define a quiver on a subset of α?)

#### Robert Spencer (Apr 08 2019 at 16:50):

The question then changes to "how do I make a Type with exactly three named elements in it"

#### Reid Barton (Apr 08 2019 at 16:51):

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#enumerated-types

#### Reid Barton (Apr 08 2019 at 16:53):

To answer your original question, ↥{A, B} is the type subtype {A, B}. To give a value of this type you need to give a value of the underlying type α together with a proof that the value belongs to the subset {A, B}--I assume by simp will do it for you.

#### Robert Spencer (Apr 08 2019 at 16:55):

Ahhhh. Sigh. Obvious now. Thank you for your time!

Last updated: May 10 2021 at 18:22 UTC