inr_mem_disjSum

Mathlib.Data.Finset.Sum

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

English

In the disjoint sum s.disjSum t, an element inr b belongs to the sum if and only if b ∈ t.

Русский

В дизъюнктивной сумме s.disjSum t элемент inr b принадлежит сумме тогда и только тогда, когда b ∈ t.

LaTeX

$$$ inr\ b \in s.disjSum t \iff b \in t $$$

Lean4

@[simp]
theorem inr_mem_disjSum : inr b ∈ s.disjSum t ↔ b ∈ t :=
  Multiset.inr_mem_disjSum

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

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

Разделы

Аффилиация

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