univ_disjSum_univ

Mathlib.Data.Fintype.Sum

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

English

The disjoint sum of the universe with itself yields the universe of the disjoint sum.

Русский

Сумма с раздельным образом единицами даёт единое множество в дизъюнктной сумме.

LaTeX

$$$\text{univ.disjSum univ} = \text{univ}$$$

Lean4

@[simp]
theorem univ_disjSum_univ : univ.disjSum univ = (univ : Finset (α ⊕ β)) :=
  rfl

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

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

Разделы

Аффилиация

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