univ_image_get' — Mathlib

English

For any l : List α and f : α → β with [DecidableEq β], the image of univ by the function i ↦ f (l.getElemNatLtLength.getElem l i.val) equals (l.map f).toFinset.

Русский

Для списка l : List α и отображения f : α → β при наличии DecidableEq β образ унив по i ↦ f (l.getElemNatLtLength.getElem l i.val) равен (l.map f).toFinset.

LaTeX

$$$$ \\operatorname{univ}.image (\\lambda i, f (\\mathrm{List}.instGetElemNatLtLength.getElem\\, l\\, i.{val})) = (l.map f).toFinset. $$$$

Lean4

theorem univ_image_get' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (f <| l.get ·) = (l.map f).toFinset := by simp

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