mem_attach

Mathlib.Data.Sym.Basic

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

English

Every element of s.attach corresponds to a member of s.

Русский

Каждый элемент в s.attach сопоставляет элементу принадлежность к s.

LaTeX

$$$\\forall x : { a \\mid a \\in s }, x \\in s.attach.$$$

Lean4

@[simp]
theorem mem_attach (s : Sym α n) (x : { x // x ∈ s }) : x ∈ s.attach :=
  Multiset.mem_attach _ _

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

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

Разделы

Аффилиация

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