univ_val_map

Mathlib.Data.Fintype.Basic

URI: https://scilib.ai/kg/mathlib#Fin.univ_val_map

English

For f : Fin n → α, Finset.univ.val.map f equals List.ofFn f.

Русский

Для f : Fin n → α, Finset.univ.val.map f эквивалентно List.ofFn f.

LaTeX

$$$\mathrm{Finset.univ}.val.map f = \mathrm{List}.ofFn f$$$

Lean4

@[simp]
theorem univ_val_map {n : ℕ} (f : Fin n → α) : Finset.univ.val.map f = List.ofFn f := by
  simp [List.ofFn_eq_map, univ_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru