English
Let S be a finite subset of a type α. The collection of elements of S, regarded as elements of the subtype {x ∈ α | x ∈ S} (i.e., attached elements), occupies the entire universe of that subtype; equivalently, the underlying set of S attached to α is the full set of all elements in the subtype.
Русский
Пусть S — конечное подмножество множества α. Набор элементов S, рассматриваемый как элементы подтипа {x ∈ α | x ∈ S} (то есть как прикреплённые элементы), заполняет всю вселенную этого подтипа; другими словами, базовое множество прикрепления S равно всем элементам подтипа.
LaTeX
$$$$ (s^{\mathrm{attach}})^{\toSet} = \mathrm{Set.univ} $$$
Lean4
@[simp, norm_cast]
theorem coe_attach (s : Finset α) : s.attach.toSet = Set.univ := by ext; simp
