Fin Universe Map Recovers List

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.NewtonIdentities

Statement

Theorem Fin Universe Map Recovers List
[blueprint]

$\bigl\{l[i] \mid i \in \mathrm{Fin}(\lvert l\rvert)\bigr\} = l$ as multisets.

theorem fin_univ_map_get (l : List ℝ) :
    (Finset.univ.val.map (fun i : Fin l.length => l.get i) : Multiset ℝ) = ↑l := by
Proof ▼ 


  rw [Fin.univ_def]
  simp only [Multiset.map_coe]
  rw [List.map_get_finRange]

Dependencies (uses)

None

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms