sumEquiv_symm_apply

Mathlib.Data.Finset.Sum

URI: https://scilib.ai/kg/mathlib#Finset.sumEquiv_symm_apply

English

Applied to a pair (s, t), the inverse of sumEquiv gives disjSum: sumEquiv.symm (s, t) = disjSum s t.

Русский

Применение к паре (s, t) обратного к сумме эквиз: sumEquiv.symm (s, t) = disjSum s t.

LaTeX

$$$\\text{sumEquiv.symm } s = \\text{disjSum } s.1 s.2$$$

Lean4

@[simp]
theorem sumEquiv_symm_apply {α β : Type*} (s : Finset α × Finset β) : sumEquiv.symm s = disjSum s.1 s.2 :=
  rfl

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

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

Разделы

Аффилиация

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