empty_disjSum

Mathlib.Data.Finset.Sum

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

English

The disjoint sum of the empty Finset with t is t.map Embedding.inr.

Русский

Дисъюнкционная сумма пустого Finset с t равна t.map Embedding.inr.

LaTeX

$$(∅ : Finset α).disjSum t = t.map Embedding.inr$$

Lean4

@[simp]
theorem empty_disjSum : (∅ : Finset α).disjSum t = t.map Embedding.inr :=
  val_inj.1 <| Multiset.zero_disjSum _

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

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

Разделы

Аффилиация

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