attach_eq_univ

Mathlib.Data.Fintype.Sets

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

English

For any finite set s, the universe of s equals its attach: s.attach = Finset.univ.

Русский

Для любого конечного множества s пространство над ним эквивалентно его attach: s.attach = Finset.univ.

LaTeX

$$$s.\mathrm{attach} = \mathrm{univ}$$$

Lean4

theorem attach_eq_univ {s : Finset α} : s.attach = Finset.univ :=
  rfl

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

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

Разделы

Аффилиация

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