## 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