Zulip Chat Archive

Stream: new members

Topic: Indexing over finite sets?


view this post on Zulip 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 a1,...,ana_1, ..., a_n. I figured I could do this by considering a finite sequence. In other words, having aa just be a function SNS\to\mathbb{N} for some finite subset SNS\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 a1+...+ana_1+... +a_n?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kristaps John Balodis (Jan 18 2021 at 22:15):

Thanks!


Last updated: May 15 2021 at 00:39 UTC