disjSum_empty

Mathlib.Data.Finset.Sum

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

English

The disjoint sum of s with the empty Finset is s.map Embedding.inl.

Русский

Дисъюнкционная сумма s с пустым Finset равна s.map Embedding.inl.

LaTeX

$$s.disjSum Finset.instEmptyCollection.emptyCollection = s.map Embedding.inl$$

Lean4

@[simp]
theorem disjSum_empty : s.disjSum (∅ : Finset β) = s.map Embedding.inl :=
  val_inj.1 <| Multiset.disjSum_zero _

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

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

Разделы

Аффилиация

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