Notion of finiteness with explicit number of elements

Stream: Is there code for X?

[Lessness]

I found the Finite which is, I believe, notion of finiteness without number of elements.

But is there something like, don't know how to name it... for example, Finite A 4 which would mean that type A has 4 different elements?

[Eric Wieser]

Can you un- #xy a little? What do you want this notion for?

[Riccardo Brasca]

If you want to assume that a finset has 4 elements just use docs#Finset.card

[Riccardo Brasca]

Or docs#Fintype.card if you have a type

[Riccardo Brasca]

Or docs#Set.ncard if you have a set (this can be a little confusing, we know).

[Eric Wieser]

ncard has a very weird type

[Lessness]

Eric Wieser said:

Can you un- #xy a little? What do you want this notion for?

I'm tinkering with directed graphs, defined as binary relation. (No clue if that's good way to define them; right now just gaining more experience and some fun with Lean.)

And I want to define a Prop like this: Digraph.Node.HasOutDegree {A: Type} (dg: Digraph A) (x: A) (n: Nat). Which would mean that { y: A // dg x y } has size n.

[Eric Wieser]

docs#Set.Sized might also work for you

[Kevin Buzzard]

Eric Wieser said:

ncard has a very weird type

Does explicitly writing : \N in the def fix things?

[Eric Wieser]

Yes, and it would be nice if there was a built-in linter for this