univ_image_get — Mathlib

English

For any list l and [DecidableEq α], the image of univ by the function l.get equals the finset of the list elements, i.e., l.toFinset.

Русский

Для любого списка l и допустимого равенства координат, образ унив по функции l.get равен множеству элементов списка, то есть l.toFinset.

LaTeX

$$$$ \\operatorname{univ}.image (l.{get}) = l.toFinset. $$$$

Lean4

@[simp]
theorem univ_image_get [DecidableEq α] (l : List α) : Finset.univ.image l.get = l.toFinset := by simp [univ_image_def]

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