antidiagonal_map_fst

Mathlib.Data.Multiset.Antidiagonal

URI: https://scilib.ai/kg/mathlib#Multiset.antidiagonal_map_fst

← MathLib Explorer

English

map fst of antidiagonal(s) equals powerset(s).

Русский

отображение по первым компонентам антидиагонали даёт powerset(s).

LaTeX

$$$$ (\operatorname{antidiagonal}(s)).\operatorname{map} \operatorname{fst} = \operatorname{powerset}(s) $$$$

Lean4

@[simp]
theorem antidiagonal_map_fst (s : Multiset α) : (antidiagonal s).map Prod.fst = powerset s :=
  Quotient.inductionOn s fun l ↦ by simp [powersetAux']

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

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

Разделы

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

Аффилиация

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