inl_mem_disjSum

Mathlib.Data.Finset.Sum

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

English

The element inl a is a member of s.disjSum t if and only if a ∈ s.

Русский

Элемент inl a принадлежит s.disjSum t тогда и только тогда, когда a ∈ s.

LaTeX

$$$\mathrm{inl}(a) \in s\disjSum t \iff a \in s$$$

Lean4

@[simp]
theorem inl_mem_disjSum : inl a ∈ s.disjSum t ↔ a ∈ s :=
  Multiset.inl_mem_disjSum

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

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

Разделы

Аффилиация

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