univ_eq_attach — Mathlib

English

For any Finset s, the Finset of its elements together with proofs equals the universal Finset over s: univ in s equals s.attach.

Русский

Для любого Finset s множества элементов вместе с доказательствами эквивалентны универсальному Finset над s: univ в s равен s.attach.

LaTeX

$$$\mathrm{univ} : \mathrm{Finset}(s) = s.\mathrm{attach}$$$

Lean4

@[simp]
theorem univ_eq_attach {α : Type u} (s : Finset α) : (univ : Finset s) = s.attach :=
  rfl

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