Indexing a Finset

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone.

Is there a way to index a Finset?

I mean, if we have some s: Finset α, does there exists a theorem that asserts that it must exist an isomorphic t: Finset ℕ :?

[Esteban Martínez Vañó]

More detail on what I want.

I've proven the following lemma:

lemma sup_bdd_one_eq_sup_bdd_le_one  {Y : Type u_6} [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f: ℕ → Y) (s: Finset ℕ) :
  sSup {t: ℝ | ∃ g: ℕ → ℝ, g '' s ⊆ {-1, 1} ∧ t = ‖∑ i ∈ s, (g i) • (f i)‖} = sSup {t: ℝ | ∃ g: ℕ → ℝ, g '' s ⊆ Icc (-1) 1 ∧ t = ‖∑ i ∈ s, (g i) • (f i)‖}

An an almost identical proof gives also:

lemma sup_bdd_one_eq_sup_bdd_le_one' {Y : Type u_6} [NormedAddCommGroup Y] [NormedSpace ℝ Y] (s: Finset Y) :
  sSup {t: ℝ | ∃ g: Y → ℝ, g '' s ⊆ {-1, 1} ∧ t = ‖∑ w ∈ s, (g w) • w‖} =  sSup {t: ℝ | ∃ g: Y → ℝ, g '' s ⊆ Icc (-1) 1 ∧ t = ‖∑ w ∈ s, (g w) • w‖}

And I think it must be possible to prove the second one via the first one without repeating all (the long) proof again by establishing a bijection between s and a Finset on the natural numbers.

Is it possible to do it in a quick way? I mean, in a way that doesn't make the second proof also long because of the needed preparation to use the first lemma.

[Yaël Dillies]

Usually, this means you should generalise an indexing type somewhere, but the answer to your titular question is docs#Fintype.equivFin

[Esteban Martínez Vañó]

Yaël Dillies ha dicho:

Usually, this means you should generalise an indexing type somewhere, but the answer to your titular question is docs#Fintype.equivFin

What do you exactly mean?

[Esteban Martínez Vañó]

Okay, I think I know what you meant. If I just change ℕ in the first lemma by a generic type, everything works okay and for the second lemma I just define f as the identity.