# Zulip Chat Archive

## Stream: new members

### Topic: Help with explicit sets

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

I've been battling a while now with `set`

s, `finset`

s, `fintype`

s 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