map_permutations'

Mathlib.Data.List.Permutation

URI: https://scilib.ai/kg/mathlib#List.map_permutations'

Lean4

theorem map_permutations' (f : α → β) (ts : List α) : map (map f) (permutations' ts) = permutations' (map f ts) := by
  induction ts with
  | nil => rfl
  | cons t ts ih => simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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