mem_toList

Mathlib.Data.Finset.Dedup

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

English

Membership in the Finset listed by toList corresponds to membership in the underlying list.

Русский

Членство в Finset через toList соответствует членству в исходном списке.

LaTeX

$$$\\forall {a : \\alpha} {s : \\mathsf{Finset}\\,\\alpha},\\; a \\in s.toList \\iff a \\in s$$$

Lean4

@[simp]
theorem mem_toList {a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s :=
  Multiset.mem_toList

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

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

Разделы

Аффилиация

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