mem_attach

Mathlib.Data.Finset.Attach

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

English

For any s : Finset α, for all x, x ∈ s.attach holds.

Русский

Для любого s : Finset α и любого x, верно: x ∈ s.attach.

LaTeX

$$$ \forall x, x \in s.\mathrm{attach} $$$

Lean4

@[simp, grind]
theorem mem_attach (s : Finset α) : ∀ x, x ∈ s.attach :=
  Multiset.mem_attach _

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

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

Разделы

Аффилиация

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