attach_val

Mathlib.Data.Finset.Attach

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

English

The underlying multiset of s.attach equals s.1.attach.

Русский

Опорный мультисет s.attach равен s.1.attach.

LaTeX

$$$ (s.\Attach).1 = s.1.attach $$$

Lean4

@[simp]
theorem attach_val (s : Finset α) : s.attach.1 = s.1.attach :=
  rfl

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

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

Разделы

Аффилиация

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