# Zulip Chat Archive

## Stream: new members

### Topic: Indexing over finite sets?

#### Kristaps John Balodis (Jan 18 2021 at 21:53):

I have a couple related questions.

First, I'm trying to prove a theorem for an arbitrary amount of finite numbers $a_1, ..., a_n$. I figured I could do this by considering a finite sequence. In other words, having $a$ just be a function $S\to\mathbb{N}$ for some *finite* subset $S\subseteq\mathbb{N}$.

However, I'm unsure of how to get a finite set. I tried looking at something like

```
constant S : finset \nat
```

but them Lean wasn't liking

```
constant a : S \to S
```

(but I don't have this problem with set \nat) So my first question is,

1) Why isn't this working?

also

2) What is the best way to grab an arbitrary index set/arbitrary finite set of naturals?

Finally,

3) How does one form a repeated sum over these? Say I want to get $a_1+... +a_n$?

#### Johan Commelin (Jan 18 2021 at 21:58):

@Kristaps John Balodis you can use something like

```
variables {X : Type*} [fintype X] (a : X \to nat)
```

#### Johan Commelin (Jan 18 2021 at 21:59):

You can sum over those by

```
import algebra.big_operators
open_locale big_operators
example : \sum i : X, a i = 0 := sorry
```

#### Kristaps John Balodis (Jan 18 2021 at 22:15):

Thanks!

Last updated: May 15 2021 at 00:39 UTC