antidiagonal_map_snd

Mathlib.Data.Multiset.Antidiagonal

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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