mem_attach

Mathlib.Data.Multiset.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.mem_attach

English

Every element of s.attach belongs to s.

Русский

Каждый элемент в s.attach принадлежит s.

LaTeX

$$$\\forall x, x\\in s.{\\text{attach}}(x)\\;\\text{(simp)}$$$

Lean4

@[simp]
theorem mem_attach (s : Multiset α) : ∀ x, x ∈ s.attach :=
  Quot.inductionOn s fun _l => List.mem_attach _

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

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

Разделы

Аффилиация

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