univ_image_getElem' — Mathlib

English

For l : List α and f : α → β, the image of univ by the map i ↦ f (l[(i : Fin l.length)]) equals theFinset of (l.map f).

Русский

Для списка l : List α и отображения f : α → β образ унив по функции i ↦ f (l[(i : Fin l.length)]) равен { значения l, преобразованных через f }.

LaTeX

$$$$ \\operatorname{univ}.image (\\lambda i : \\mathrm{Fin} (l.length), f (l[(i : \\mathrm{Nat})])) = (l.map\\; f).toFinset. $$$$

Lean4

@[simp]
theorem univ_image_getElem' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (fun i : Fin l.length => f <| l[(i : Nat)]) = (l.map f).toFinset := by
  simp only [univ_image_def, List.ofFn_getElem_eq_map]

Похожие утверждения